diff options
Diffstat (limited to 'compiler/InterpreterExpansion.ml')
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 239 |
1 files changed, 98 insertions, 141 deletions
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index e47fbfbe..39c9bd4a 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -191,8 +191,8 @@ let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) ctx let apply_symbolic_expansion_non_borrow (config : config) (meta : Meta.meta) - (original_sv : symbolic_value) (expansion : symbolic_expansion) - (ctx : eval_ctx) : eval_ctx = + (original_sv : symbolic_value) (ctx : eval_ctx) + (expansion : symbolic_expansion) : eval_ctx = (* Apply the expansion to non-abstraction values *) let nv = symbolic_expansion_non_borrow_to_value meta original_sv expansion in let at_most_once = false in @@ -288,7 +288,7 @@ let compute_expanded_symbolic_adt_value (meta : Meta.meta) let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) (original_sv : symbolic_value) (original_sv_place : SA.mplace option) (ref_ty : rty) : cm_fun = - fun cf ctx -> + fun 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 @@ -395,17 +395,16 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv see ctx in - (* Call the continuation *) - let expr = cf ctx in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching meta original_sv - original_sv_place see expr + ( ctx, + (* Update the synthesized program *) + S.synthesize_symbolic_expansion_no_branching meta original_sv + original_sv_place see ) (** TODO: simplify and merge with the other expansion function *) let expand_symbolic_value_borrow (config : config) (meta : Meta.meta) (original_sv : symbolic_value) (original_sv_place : SA.mplace option) (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun = - fun cf ctx -> + fun ctx -> sanity_check __FILE__ __LINE__ (region <> RErased) meta; (* Check that we are allowed to expand the reference *) sanity_check __FILE__ __LINE__ @@ -435,99 +434,47 @@ let expand_symbolic_value_borrow (config : config) (meta : Meta.meta) original_sv see ctx in (* Apply the continuation *) - let expr = cf ctx in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching meta original_sv - original_sv_place see expr + ( ctx, + fun e -> + (* Update the synthesized program *) + S.synthesize_symbolic_expansion_no_branching meta original_sv + original_sv_place see e ) | RShared -> expand_symbolic_value_shared_borrow config meta original_sv - original_sv_place ref_ty cf ctx - -(** A small helper. - - Apply a branching symbolic expansion to a context and execute all the - 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). - 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 : config) - (meta : Meta.meta) (sv : symbolic_value) (sv_place : SA.mplace option) - (see_cf_l : (symbolic_expansion option * st_cm_fun) list) - (cf_after_join : st_m_fun) : m_fun = - fun ctx -> - sanity_check __FILE__ __LINE__ (see_cf_l <> []) meta; - (* Apply the symbolic expansion in the context and call the continuation *) - let resl = - List.map - (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 meta 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 ~meta:(Some meta) ctx0 - ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx - ^ "\n")); - (* Continuation *) - cf_br cf_after_join ctx) - see_cf_l - in - (* Collect the result: either we computed no subterm, or we computed all - * of them *) - let subterms = - match resl with - | Some _ :: _ -> Some (List.map Option.get resl) - | None :: _ -> - List.iter - (fun res -> sanity_check __FILE__ __LINE__ (res = None) meta) - resl; - None - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - (* Synthesize and return *) - let seel = List.map fst see_cf_l in - S.synthesize_symbolic_expansion meta sv sv_place seel subterms + original_sv_place ref_ty ctx let expand_symbolic_bool (config : config) (meta : Meta.meta) - (sv : symbolic_value) (sv_place : SA.mplace option) (cf_true : st_cm_fun) - (cf_false : st_cm_fun) (cf_after_join : st_m_fun) : m_fun = + (sv : symbolic_value) (sv_place : SA.mplace option) : + eval_ctx -> + (eval_ctx * eval_ctx) + * ((SymbolicAst.expression * SymbolicAst.expression) option -> eval_result) + = fun ctx -> (* Compute the expanded value *) let original_sv = sv in - let original_sv_place = sv_place in let rty = original_sv.sv_ty in sanity_check __FILE__ __LINE__ (rty = TLiteral TBool) meta; (* Expand the symbolic value to true or false and continue execution *) let see_true = SeLiteral (VBool true) in let see_false = SeLiteral (VBool false) in - 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 meta original_sv - original_sv_place seel cf_after_join ctx + let seel = [ Some see_true; Some see_false ] in + (* Apply the symbolic expansion *) + let apply_expansion = + apply_symbolic_expansion_non_borrow config meta sv ctx + in + let ctx_true = apply_expansion see_true in + let ctx_false = apply_expansion see_false in + (* Compute the continuation to build the expression *) + let cf e = + let el = match e with Some (a, b) -> Some [ a; b ] | None -> None in + S.synthesize_symbolic_expansion meta sv sv_place seel el + in + (* Return *) + ((ctx_true, ctx_false), cf) let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv : symbolic_value) (sv_place : SA.mplace option) : cm_fun = - fun cf ctx -> + fun ctx -> (* Debug *) log#ldebug (lazy @@ -539,8 +486,7 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) let original_sv = sv in let original_sv_place = sv_place in let rty = original_sv.sv_ty in - let cc : cm_fun = - fun cf ctx -> + let ctx, cc = match rty with (* ADTs *) | TAdt (adt_id, generics) -> @@ -554,45 +500,43 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) let see = Collections.List.to_cons_nil seel in (* Apply in the context *) let ctx = - apply_symbolic_expansion_non_borrow config meta original_sv see ctx + apply_symbolic_expansion_non_borrow config meta original_sv ctx see in - (* Call the continuation *) - let expr = cf ctx in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching meta original_sv - original_sv_place see expr + (* Return*) + ( ctx, + (* Update the synthesized program *) + S.synthesize_symbolic_expansion_no_branching meta original_sv + original_sv_place see ) (* Borrows *) | TRef (region, ref_ty, rkind) -> expand_symbolic_value_borrow config meta original_sv original_sv_place - region ref_ty rkind cf ctx + region ref_ty rkind ctx | _ -> craise __FILE__ __LINE__ meta ("expand_symbolic_value_no_branching: unexpected type: " ^ show_rty rty) in (* Debug *) - let cc = - comp_unit cc (fun ctx -> - log#ldebug - (lazy - ("expand_symbolic_value_no_branching: " - ^ symbolic_value_to_string ctx0 sv - ^ "\n\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 - ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx - ^ "\n")); - (* Sanity check: the symbolic value has disappeared *) - sanity_check __FILE__ __LINE__ - (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) - meta) - in - (* Continue *) - cc cf ctx + log#ldebug + (lazy + ("expand_symbolic_value_no_branching: " + ^ symbolic_value_to_string ctx0 sv + ^ "\n\n- original context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ "\n")); + (* Sanity check: the symbolic value has disappeared *) + sanity_check __FILE__ __LINE__ + (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) + meta; + (* Return *) + (ctx, cc) let expand_symbolic_adt (config : config) (meta : Meta.meta) - (sv : symbolic_value) (sv_place : SA.mplace option) - (cf_branches : st_cm_fun) (cf_after_join : st_m_fun) : m_fun = + (sv : symbolic_value) (sv_place : SA.mplace option) : + eval_ctx -> + eval_ctx list * (SymbolicAst.expression list option -> eval_result) = fun ctx -> (* Debug *) log#ldebug (lazy ("expand_symbolic_adt:" ^ symbolic_value_to_string ctx sv)); @@ -612,17 +556,24 @@ let expand_symbolic_adt (config : config) (meta : Meta.meta) ctx in (* Apply *) - let seel = List.map (fun see -> (Some see, cf_branches)) seel in - apply_branching_symbolic_expansions_non_borrow config meta original_sv - original_sv_place seel cf_after_join ctx + let ctx_branches = + List.map (apply_symbolic_expansion_non_borrow config meta sv ctx) seel + in + ( ctx_branches, + S.synthesize_symbolic_expansion meta sv original_sv_place + (List.map (fun el -> Some el) seel) ) | _ -> craise __FILE__ __LINE__ meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty) let expand_symbolic_int (config : config) (meta : Meta.meta) (sv : symbolic_value) (sv_place : SA.mplace option) - (int_type : integer_type) (tgts : (scalar_value * st_cm_fun) list) - (otherwise : st_cm_fun) (cf_after_join : st_m_fun) : m_fun = + (int_type : integer_type) (tgts : scalar_value list) : + eval_ctx -> + (eval_ctx list * eval_ctx) + * ((SymbolicAst.expression list * SymbolicAst.expression) option -> + eval_result) = + fun ctx -> (* Sanity check *) sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral (TInteger int_type)) meta; (* For all the branches of the switch, we expand the symbolic value @@ -630,17 +581,23 @@ let expand_symbolic_int (config : config) (meta : Meta.meta) * For the otherwise branch, we leave the symbolic value as it is * (because this branch doesn't precisely define which should be the * value of the scrutinee...) and simply execute the otherwise statement. - * - * First, generate the list of pairs: - * (optional expansion, statement to execute) *) - let seel = - List.map (fun (v, cf) -> (Some (SeLiteral (VScalar v)), cf)) tgts + (* Substitute the symbolic values to generate the contexts in the branches *) + let seel = List.map (fun v -> SeLiteral (VScalar v)) tgts in + let ctx_branches = + List.map (apply_symbolic_expansion_non_borrow config meta sv ctx) seel 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 meta sv sv_place seel - cf_after_join + let ctx_otherwise = ctx in + (* Update the symbolic ast *) + let cf e = + match e with + | None -> None + | Some (el, e) -> + let seel = List.map (fun x -> Some x) seel in + S.synthesize_symbolic_expansion meta sv sv_place (seel @ [ None ]) + (Some (el @ [ e ])) + in + ((ctx_branches, ctx_otherwise), cf) (** Expand all the symbolic values which contain borrows. Allows us to restrict ourselves to a simpler model for the projectors over @@ -652,7 +609,7 @@ let expand_symbolic_int (config : config) (meta : Meta.meta) *) let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : cm_fun = - fun cf ctx -> + fun ctx -> (* The visitor object, to look for symbolic values in the concrete environment *) let obj = object @@ -669,20 +626,20 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : in let rec expand : cm_fun = - fun cf ctx -> + fun ctx -> try (* We reverse the environment before exploring it - this way the values get expanded in a more "logical" order (this is only for convenience) *) obj#visit_env () (List.rev ctx.env); (* Nothing to expand: continue *) - cf ctx + (ctx, fun e -> e) with FoundSymbolicValue sv -> (* Expand and recheck the environment *) log#ldebug (lazy ("greedy_expand_symbolics_with_borrows: about to expand: " ^ symbolic_value_to_string ctx sv)); - let cc : cm_fun = + let ctx, cc = match sv.sv_ty with | TAdt (TAdtId def_id, _) -> (* {!expand_symbolic_value_no_branching} checks if there are branchings, @@ -706,10 +663,10 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : ("Attempted to greedily expand a recursive definition (option \ [greedy_expand_symbolics_with_borrows] of [config]): " ^ name_to_string ctx def.name) - else expand_symbolic_value_no_branching config meta sv None + else expand_symbolic_value_no_branching config meta sv None ctx | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) -> (* Ok *) - expand_symbolic_value_no_branching config meta sv None + expand_symbolic_value_no_branching config meta sv None ctx | TAdt (TAssumed (TArray | TSlice | TStr), _) -> (* We can't expand those *) craise __FILE__ __LINE__ meta @@ -718,15 +675,15 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : craise __FILE__ __LINE__ meta "Unreachable" in (* Compose and continue *) - comp cc expand cf ctx + comp cc (expand ctx) in (* Apply *) - expand cf ctx + expand ctx let greedy_expand_symbolic_values (config : config) (meta : Meta.meta) : cm_fun = - fun cf ctx -> + fun ctx -> if Config.greedy_expand_symbolics_with_borrows then ( log#ldebug (lazy "greedy_expand_symbolic_values"); - greedy_expand_symbolics_with_borrows config meta cf ctx) - else cf ctx + greedy_expand_symbolics_with_borrows config meta ctx) + else (ctx, fun e -> e) |