From 239435fc667fa0d18979e603ce3fd4caa128cd54 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 23 May 2024 23:21:12 +0200 Subject: Update the interpreter so that it is not written in CPS style (#120) * Start turning the compiler in a style which is less CPS * Update a function in InterpreterExpressions.ml * WIP work on cps * WIP * WIP, currently on InterpreterStatements.ml * WIP * Finished CPS-related modification * Fixed some warning related to documentation comments * Finished loop support, fixed a loop * fixed a typed value * Fixed check_disappeared related error * cleaned check_disappeared related error * Start cleaning up * Do more cleanup * Make some cleanup and fix an issue * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Rename a function * Do more cleanup * Cleanup the loops code and fix some bugs * Cleanup assign_to_place * Make a minor cleanup --------- Co-authored-by: Son Ho --- compiler/InterpreterExpansion.mli | 46 +++++++++++++++------------------------ 1 file changed, 17 insertions(+), 29 deletions(-) (limited to 'compiler/InterpreterExpansion.mli') diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli index 2ea27ea6..7140d55f 100644 --- a/compiler/InterpreterExpansion.mli +++ b/compiler/InterpreterExpansion.mli @@ -15,8 +15,8 @@ val apply_symbolic_expansion_non_borrow : config -> Meta.meta -> symbolic_value -> - symbolic_expansion -> eval_ctx -> + symbolic_expansion -> eval_ctx (** Expand a symhbolic value, without branching *) @@ -28,38 +28,30 @@ val expand_symbolic_value_no_branching : Parameters: - [config] + - [meta] - [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 : config -> Meta.meta -> symbolic_value -> SA.mplace option -> - st_cm_fun -> - st_m_fun -> - m_fun + eval_ctx -> + eval_ctx list * (SymbolicAst.expression list option -> eval_result) (** 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 : config -> Meta.meta -> symbolic_value -> SA.mplace option -> - st_cm_fun -> - st_cm_fun -> - st_m_fun -> - m_fun + eval_ctx -> + (eval_ctx * eval_ctx) + * ((SymbolicAst.expression * SymbolicAst.expression) option -> eval_result) (** Symbolic integers are expanded upon evaluating a [SwitchInt]. @@ -69,16 +61,11 @@ val expand_symbolic_bool : then retry evaluating the [if ... then ... else ...] or the [match]: as the scrutinee will then have a concrete value, the interpreter will switch to the proper branch. - - However, when expanding a "regular" integer for a switch, there is always an - *otherwise* branch that we can take, for which the integer must remain symbolic - (because in this branch the scrutinee can take a range of values). We thus - can't simply expand then retry to evaluate the [switch], because then we - would loop... - - For this reason, we take the list of branches to execute as parameters, and - directly jump to those branches after the expansion, without reevaluating the - switch. The continuation is thus for the execution *after* the switch. + + When expanding a "regular" integer for a switch there is always an *otherwise* + branch. We treat it separately: for this reason we return a pair of a list + of evaluation contexts (for the branches which are not the otherwise branch) + and an additional evaluation context for the otherwise branch. *) val expand_symbolic_int : config -> @@ -86,10 +73,11 @@ val expand_symbolic_int : symbolic_value -> SA.mplace option -> integer_type -> - (scalar_value * st_cm_fun) list -> - st_cm_fun -> - st_m_fun -> - m_fun + scalar_value list -> + eval_ctx -> + (eval_ctx list * eval_ctx) + * ((SymbolicAst.expression list * SymbolicAst.expression) option -> + eval_result) (** If this mode is activated through the [config], greedily expand the symbolic values which need to be expanded. See {!type:Contexts.config} for more information. -- cgit v1.2.3 From b294639a5cbd2a51fc5bb5e55e0c386ee568ca8c Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 24 May 2024 13:28:12 +0200 Subject: Rename meta into span --- compiler/InterpreterExpansion.mli | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'compiler/InterpreterExpansion.mli') diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli index 7140d55f..7f8c3a0a 100644 --- a/compiler/InterpreterExpansion.mli +++ b/compiler/InterpreterExpansion.mli @@ -13,7 +13,7 @@ type proj_kind = LoanProj | BorrowProj *) val apply_symbolic_expansion_non_borrow : config -> - Meta.meta -> + Meta.span -> symbolic_value -> eval_ctx -> symbolic_expansion -> @@ -21,20 +21,20 @@ val apply_symbolic_expansion_non_borrow : (** Expand a symhbolic value, without branching *) val expand_symbolic_value_no_branching : - config -> Meta.meta -> symbolic_value -> SA.mplace option -> cm_fun + config -> Meta.span -> symbolic_value -> SA.mplace option -> cm_fun (** Expand a symbolic enumeration (leads to branching if the enumeration has more than one variant). Parameters: - [config] - - [meta] + - [span] - [sv] - [sv_place] *) val expand_symbolic_adt : config -> - Meta.meta -> + Meta.span -> symbolic_value -> SA.mplace option -> eval_ctx -> @@ -46,7 +46,7 @@ val expand_symbolic_adt : *) val expand_symbolic_bool : config -> - Meta.meta -> + Meta.span -> symbolic_value -> SA.mplace option -> eval_ctx -> @@ -69,7 +69,7 @@ val expand_symbolic_bool : *) val expand_symbolic_int : config -> - Meta.meta -> + Meta.span -> symbolic_value -> SA.mplace option -> integer_type -> @@ -82,4 +82,4 @@ val expand_symbolic_int : (** If this mode is activated through the [config], greedily expand the symbolic values which need to be expanded. See {!type:Contexts.config} for more information. *) -val greedy_expand_symbolic_values : config -> Meta.meta -> cm_fun +val greedy_expand_symbolic_values : config -> Meta.span -> cm_fun -- cgit v1.2.3