diff options
Diffstat (limited to 'compiler/InterpreterStatements.ml')
| -rw-r--r-- | compiler/InterpreterStatements.ml | 1370 |
1 files changed, 1370 insertions, 0 deletions
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml new file mode 100644 index 00000000..4e61e683 --- /dev/null +++ b/compiler/InterpreterStatements.ml @@ -0,0 +1,1370 @@ +module T = Types +module V = Values +module E = Expressions +module C = Contexts +module Subst = Substitute +module A = LlbcAst +module L = Logging +open TypesUtils +open ValuesUtils +module Inv = Invariants +module S = SynthesizeSymbolic +open Errors +open Cps +open InterpreterUtils +open InterpreterProjectors +open InterpreterExpansion +open InterpreterPaths +open InterpreterExpressions + +(** The local logger *) +let log = L.statements_log + +(** Drop a value at a given place - TODO: factorize this with [assign_to_place] *) +let drop_value (config : C.config) (p : E.place) : cm_fun = + fun cf ctx -> + log#ldebug + (lazy + ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n" + ^ eval_ctx_to_string ctx)); + (* Prepare the place (by ending the outer loans). + * Note that {!prepare_lplace} will use the [Write] access kind: + * it is ok, because when updating the value with {!Bottom} below, + * we will use the [Move] access *) + let end_borrows = false in + let prepare = prepare_lplace config end_borrows p in + (* Replace the value with {!Bottom} *) + let replace cf (v : V.typed_value) ctx = + (* Move the value at destination (that we will overwrite) to a dummy variable + * to preserve the borrows *) + let mv = read_place_unwrap config Write p ctx in + let ctx = C.ctx_push_dummy_var ctx mv in + (* Update the destination to ⊥ *) + let nv = { v with value = V.Bottom } in + let ctx = write_place_unwrap config Move p nv ctx in + log#ldebug + (lazy + ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n" + ^ eval_ctx_to_string ctx)); + cf ctx + in + (* Compose and apply *) + comp prepare replace cf ctx + +(** Push a dummy variable to the environment *) +let push_dummy_var (v : V.typed_value) : cm_fun = + fun cf ctx -> + let ctx = C.ctx_push_dummy_var ctx v in + cf ctx + +(** Pop a dummy variable from the environment *) +let pop_dummy_var (cf : V.typed_value -> m_fun) : m_fun = + fun ctx -> + let ctx, v = C.ctx_pop_dummy_var ctx in + cf v ctx + +(** Push an uninitialized variable to the environment *) +let push_uninitialized_var (var : A.var) : cm_fun = + fun cf ctx -> + let ctx = C.ctx_push_uninitialized_var ctx var in + cf ctx + +(** Push a list of uninitialized variables to the environment *) +let push_uninitialized_vars (vars : A.var list) : cm_fun = + fun cf ctx -> + let ctx = C.ctx_push_uninitialized_vars ctx vars in + cf ctx + +(** Push a variable to the environment *) +let push_var (var : A.var) (v : V.typed_value) : cm_fun = + fun cf ctx -> + let ctx = C.ctx_push_var ctx var v in + cf ctx + +(** Push a list of variables to the environment *) +let push_vars (vars : (A.var * V.typed_value) list) : cm_fun = + fun cf ctx -> + let ctx = C.ctx_push_vars ctx vars in + cf ctx + +(** Assign a value to a given place. + + Note that this function first pushes the value to assign in a dummy variable, + then prepares the destination (by ending borrows, etc.) before popping the + dummy variable and putting in its destination (after having checked that + preparing the destination didn't introduce ⊥). + *) +let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) : + cm_fun = + fun cf ctx -> + log#ldebug + (lazy + ("assign_to_place:" ^ "\n- rv: " + ^ typed_value_to_string ctx rv + ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Initial context:\n" + ^ eval_ctx_to_string ctx)); + (* Push the rvalue to a dummy variable, for bookkeeping *) + let cc = push_dummy_var rv in + (* Prepare the destination *) + let end_borrows = false in + let cc = comp cc (prepare_lplace config end_borrows p) in + (* Retrieve the rvalue from the dummy variable *) + let cc = comp cc (fun cf _lv -> pop_dummy_var cf) in + (* Update the destination *) + let move_dest cf (rv : V.typed_value) : m_fun = + fun ctx -> + (* Move the value at destination (that we will overwrite) to a dummy variable + * to preserve the borrows *) + let mv = read_place_unwrap config Write p ctx in + let ctx = C.ctx_push_dummy_var ctx mv in + (* Write to the destination *) + (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) + assert (not (bottom_in_value ctx.ended_regions rv)); + (* Update the destination *) + let ctx = write_place_unwrap config Write p rv ctx in + (* Debug *) + log#ldebug + (lazy + ("assign_to_place:" ^ "\n- rv: " + ^ typed_value_to_string ctx rv + ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n" + ^ eval_ctx_to_string ctx)); + (* Continue *) + cf ctx + in + (* Compose and apply *) + comp cc move_dest cf ctx + +(** Evaluate an assertion, when the scrutinee is not symbolic *) +let eval_assertion_concrete (config : C.config) (assertion : A.assertion) : + st_cm_fun = + fun cf ctx -> + (* There won't be any symbolic expansions: fully evaluate the operand *) + let eval_op = eval_operand config assertion.cond in + let eval_assert cf (v : V.typed_value) : m_fun = + fun ctx -> + match v.value with + | Concrete (Bool b) -> + (* Branch *) + if b = assertion.expected then cf Unit ctx else cf Panic ctx + | _ -> + raise + (Failure ("Expected a boolean, got: " ^ typed_value_to_string ctx v)) + in + (* Compose and apply *) + comp eval_op eval_assert cf ctx + +(** Evaluates an assertion. + + In the case the boolean under scrutinee is symbolic, we synthesize + a call to [assert ...] then continue in the success branch (and thus + expand the boolean to [true]). + *) +let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun = + fun cf ctx -> + (* Evaluate the operand *) + let eval_op = eval_operand config assertion.cond in + (* Evaluate the assertion *) + let eval_assert cf (v : V.typed_value) : m_fun = + fun ctx -> + assert (v.ty = T.Bool); + (* We make a choice here: we could completely decouple the concrete and + * symbolic executions here but choose not to. In the case where we + * know the concrete value of the boolean we test, we use this value + * even if we are in symbolic mode. Note that this case should be + * extremely rare... *) + match v.value with + | Concrete (Bool _) -> + (* Delegate to the concrete evaluation function *) + eval_assertion_concrete config assertion cf ctx + | Symbolic sv -> + assert (config.mode = C.SymbolicMode); + assert (sv.V.sv_ty = T.Bool); + (* Expand the symbolic value and call the proper continuation functions + * for the true and false cases - TODO: call an "assert" function instead *) + let cf_true : m_fun = fun ctx -> cf Unit ctx in + let cf_false : m_fun = fun ctx -> cf Panic ctx in + let expand = + expand_symbolic_bool config sv + (S.mk_opt_place_from_op assertion.cond ctx) + cf_true cf_false + in + expand ctx + | _ -> + raise + (Failure ("Expected a boolean, got: " ^ typed_value_to_string ctx v)) + in + (* Compose and apply *) + comp eval_op eval_assert cf ctx + +(** Updates the discriminant of a value at a given place. + + There are two situations: + - either the discriminant is already the proper one (in which case we + don't do anything) + - or it is not the proper one (because the variant is not the proper + one, or the value is actually {!V.Bottom} - this happens when + initializing ADT values), in which case we replace the value with + a variant with all its fields set to {!V.Bottom}. + For instance, something like: [Cons Bottom Bottom]. + *) +let set_discriminant (config : C.config) (p : E.place) + (variant_id : T.VariantId.id) : st_cm_fun = + fun cf ctx -> + log#ldebug + (lazy + ("set_discriminant:" ^ "\n- p: " ^ place_to_string ctx p + ^ "\n- variant id: " + ^ T.VariantId.to_string variant_id + ^ "\n- initial context:\n" ^ eval_ctx_to_string ctx)); + (* Access the value *) + let access = Write in + let cc = update_ctx_along_read_place config access p in + let end_borrows = false in + let cc = comp cc (prepare_lplace config end_borrows p) in + (* Update the value *) + let update_value cf (v : V.typed_value) : m_fun = + fun ctx -> + match (v.V.ty, v.V.value) with + | ( T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), regions, types), + V.Adt av ) -> ( + (* There are two situations: + - either the discriminant is already the proper one (in which case we + don't do anything) + - or it is not the proper one, in which case we replace the value with + a variant with all its fields set to {!Bottom} + *) + match av.variant_id with + | None -> raise (Failure "Found a struct value while expected an enum") + | Some variant_id' -> + if variant_id' = variant_id then (* Nothing to do *) + cf Unit ctx + else + (* Replace the value *) + let bottom_v = + match type_id with + | T.AdtId def_id -> + compute_expanded_bottom_adt_value + ctx.type_context.type_decls def_id (Some variant_id) + regions types + | T.Assumed T.Option -> + assert (regions = []); + compute_expanded_bottom_option_value variant_id + (Collections.List.to_cons_nil types) + | _ -> raise (Failure "Unreachable") + in + assign_to_place config bottom_v p (cf Unit) ctx) + | ( T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), regions, types), + V.Bottom ) -> + let bottom_v = + match type_id with + | T.AdtId def_id -> + compute_expanded_bottom_adt_value ctx.type_context.type_decls + def_id (Some variant_id) regions types + | T.Assumed T.Option -> + assert (regions = []); + compute_expanded_bottom_option_value variant_id + (Collections.List.to_cons_nil types) + | _ -> raise (Failure "Unreachable") + in + assign_to_place config bottom_v p (cf Unit) ctx + | _, V.Symbolic _ -> + assert (config.mode = SymbolicMode); + (* This is a bit annoying: in theory we should expand the symbolic value + * then set the discriminant, because in the case the discriminant is + * exactly the one we set, the fields are left untouched, and in the + * other cases they are set to Bottom. + * For now, we forbid setting the discriminant of a symbolic value: + * setting a discriminant should only be used to initialize a value, + * or reset an already initialized value, really. *) + raise (Failure "Unexpected value") + | _, (V.Adt _ | V.Bottom) -> raise (Failure "Inconsistent state") + | _, (V.Concrete _ | V.Borrow _ | V.Loan _) -> + raise (Failure "Unexpected value") + in + (* Compose and apply *) + comp cc update_value cf ctx + +(** Push a frame delimiter in the context's environment *) +let ctx_push_frame (ctx : C.eval_ctx) : C.eval_ctx = + { ctx with env = Frame :: ctx.env } + +(** Push a frame delimiter in the context's environment *) +let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx) + +(** Small helper: compute the type of the return value for a specific + instantiation of a non-local function. + *) +let get_non_local_function_return_type (fid : A.assumed_fun_id) + (region_params : T.erased_region list) (type_params : T.ety list) : T.ety = + (* [Box::free] has a special treatment *) + match (fid, region_params, type_params) with + | A.BoxFree, [], [ _ ] -> mk_unit_ty + | _ -> + (* Retrieve the function's signature *) + let sg = Assumed.get_assumed_sig fid in + (* Instantiate the return type *) + let tsubst = + Subst.make_type_subst + (List.map (fun v -> v.T.index) sg.type_params) + type_params + in + Subst.erase_regions_substitute_types tsubst sg.output + +let move_return_value (config : C.config) (cf : V.typed_value -> m_fun) : m_fun + = + fun ctx -> + let ret_vid = V.VarId.zero in + let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in + cc cf ctx + +(** Pop the current frame. + + Drop all the local variables but the return variable, move the return + value out of the return variable, remove all the local variables (but not the + abstractions!) from the context, remove the {!C.Frame} indicator delimiting the + current frame and handle the return value to the continuation. + + TODO: rename (remove the "ctx_") + *) +let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun = + fun ctx -> + (* Debug *) + log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx)); + + (* List the local variables, but the return variable *) + let ret_vid = V.VarId.zero in + let rec list_locals env = + match env with + | [] -> raise (Failure "Inconsistent environment") + | C.Abs _ :: env -> list_locals env + | C.Var (None, _) :: env -> list_locals env + | C.Var (Some var, _) :: env -> + let locals = list_locals env in + if var.index <> ret_vid then var.index :: locals else locals + | C.Frame :: _ -> [] + in + let locals : V.VarId.id list = list_locals ctx.env in + (* Debug *) + log#ldebug + (lazy + ("ctx_pop_frame: locals in which to drop the outer loans: [" + ^ String.concat "," (List.map V.VarId.to_string locals) + ^ "]")); + + (* Move the return value out of the return variable *) + let cc = move_return_value config in + (* Sanity check *) + let cc = + comp_check_value cc (fun ret_value ctx -> + assert (not (bottom_in_value ctx.ended_regions ret_value))) + in + + (* Drop the outer *loans* we find in the local variables *) + let cf_drop_loans_in_locals cf (ret_value : V.typed_value) : m_fun = + (* Drop the loans *) + let end_borrows = false in + let locals = List.rev locals in + let cf_drop = + List.fold_left + (fun cf lid -> + drop_outer_borrows_loans_at_lplace config end_borrows + (mk_place_from_var_id lid) cf) + (cf ret_value) locals + in + (* Apply *) + cf_drop + in + let cc = comp cc cf_drop_loans_in_locals in + (* Debug *) + let cc = + comp_check_value cc (fun _ ctx -> + log#ldebug + (lazy + ("ctx_pop_frame: after dropping outer loans in local variables:\n" + ^ eval_ctx_to_string ctx))) + in + + (* Pop the frame - we remove the [Frame] delimiter, and reintroduce all + * the local variables (which may still contain borrow permissions - but + * no outer loans) as dummy variables in the caller frame *) + let rec pop env = + match env with + | [] -> raise (Failure "Inconsistent environment") + | C.Abs abs :: env -> C.Abs abs :: pop env + | C.Var (_, v) :: env -> C.Var (None, v) :: pop env + | C.Frame :: env -> (* Stop here *) env + in + let cf_pop cf (ret_value : V.typed_value) : m_fun = + fun ctx -> + let env = pop ctx.env in + let ctx = { ctx with env } in + cf ret_value ctx + in + (* Compose and apply *) + comp cc cf_pop cf ctx + +(** Pop the current frame and assign the returned value to its destination. *) +let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun = + let cf_pop = ctx_pop_frame config in + let cf_assign cf ret_value : m_fun = + assign_to_place config ret_value dest cf + in + comp cf_pop cf_assign + +(** Auxiliary function - see [eval_non_local_function_call] *) +let eval_replace_concrete (_config : C.config) + (_region_params : T.erased_region list) (_type_params : T.ety list) : cm_fun + = + fun _cf _ctx -> raise Unimplemented + +(** Auxiliary function - see [eval_non_local_function_call] *) +let eval_box_new_concrete (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun = + fun cf ctx -> + (* Check and retrieve the arguments *) + match (region_params, type_params, ctx.env) with + | ( [], + [ boxed_ty ], + Var (Some input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) + -> + (* Required type checking *) + assert (input_value.V.ty = boxed_ty); + + (* Move the input value *) + let cf_move = + eval_operand config (E.Move (mk_place_from_var_id input_var.C.index)) + in + + (* Create the new box *) + let cf_create cf (moved_input_value : V.typed_value) : m_fun = + (* Create the box value *) + let box_ty = T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) in + let box_v = + V.Adt { variant_id = None; field_values = [ moved_input_value ] } + in + let box_v = mk_typed_value box_ty box_v in + + (* Move this value to the return variable *) + let dest = mk_place_from_var_id V.VarId.zero in + let cf_assign = assign_to_place config box_v dest in + + (* Continue *) + cf_assign cf + in + + (* Compose and apply *) + comp cf_move cf_create cf ctx + | _ -> raise (Failure "Inconsistent state") + +(** Auxiliary function which factorizes code to evaluate [std::Deref::deref] + and [std::DerefMut::deref_mut] - see [eval_non_local_function_call] *) +let eval_box_deref_mut_or_shared_concrete (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) + (is_mut : bool) : cm_fun = + fun cf ctx -> + (* Check the arguments *) + match (region_params, type_params, ctx.env) with + | ( [], + [ boxed_ty ], + Var (Some input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) + -> + (* Required type checking. We must have: + - input_value.ty == & (mut) Box<ty> + - boxed_ty == ty + for some ty + *) + (let _, input_ty, ref_kind = ty_get_ref input_value.V.ty in + assert (match ref_kind with T.Shared -> not is_mut | T.Mut -> is_mut); + let input_ty = ty_get_box input_ty in + assert (input_ty = boxed_ty)); + + (* Borrow the boxed value *) + let p = + { E.var_id = input_var.C.index; projection = [ E.Deref; E.DerefBox ] } + in + let borrow_kind = if is_mut then E.Mut else E.Shared in + let rv = E.Ref (p, borrow_kind) in + let cf_borrow = eval_rvalue config rv in + + (* Move the borrow to its destination *) + let cf_move cf res : m_fun = + match res with + | Error EPanic -> + (* We can't get there by borrowing a value *) + raise (Failure "Unreachable") + | Ok borrowed_value -> + (* Move and continue *) + let destp = mk_place_from_var_id V.VarId.zero in + assign_to_place config borrowed_value destp cf + in + + (* Compose and apply *) + comp cf_borrow cf_move cf ctx + | _ -> raise (Failure "Inconsistent state") + +(** Auxiliary function - see [eval_non_local_function_call] *) +let eval_box_deref_concrete (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun = + let is_mut = false in + eval_box_deref_mut_or_shared_concrete config region_params type_params is_mut + +(** Auxiliary function - see [eval_non_local_function_call] *) +let eval_box_deref_mut_concrete (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun = + let is_mut = true in + eval_box_deref_mut_or_shared_concrete config region_params type_params is_mut + +(** Auxiliary function - see [eval_non_local_function_call]. + + [Box::free] is not handled the same way as the other assumed functions: + - in the regular case, whenever we need to evaluate an assumed function, + we evaluate the operands, push a frame, call a dedicated function + to correctly update the variables in the frame (and mimic the execution + of a body) and finally pop the frame + - in the case of [Box::free]: the value given to this function is often + of the form [Box(⊥)] because we can move the value out of the + box before freeing the box. It makes it invalid to see box_free as a + "regular" function: it is not valid to call a function with arguments + which contain [⊥]. For this reason, we execute [Box::free] as drop_value, + but this is a bit annoying with regards to the semantics... + + Followingly this function doesn't behave like the others: it does not expect + a stack frame to have been pushed, but rather simply behaves like {!drop_value}. + It thus updates the box value (by calling {!drop_value}) and updates + the destination (by setting it to [()]). +*) +let eval_box_free (config : C.config) (region_params : T.erased_region list) + (type_params : T.ety list) (args : E.operand list) (dest : E.place) : cm_fun + = + fun cf ctx -> + match (region_params, type_params, args) with + | [], [ boxed_ty ], [ E.Move input_box_place ] -> + (* Required type checking *) + let input_box = read_place_unwrap config Write input_box_place ctx in + (let input_ty = ty_get_box input_box.V.ty in + assert (input_ty = boxed_ty)); + + (* Drop the value *) + let cc = drop_value config input_box_place in + + (* Update the destination by setting it to [()] *) + let cc = comp cc (assign_to_place config mk_unit_value dest) in + + (* Continue *) + cc cf ctx + | _ -> raise (Failure "Inconsistent state") + +(** Auxiliary function - see [eval_non_local_function_call] *) +let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) + (_region_params : T.erased_region list) (_type_params : T.ety list) : cm_fun + = + fun _cf _ctx -> raise Unimplemented + +(** Evaluate a non-local function call in concrete mode *) +let eval_non_local_function_call_concrete (config : C.config) + (fid : A.assumed_fun_id) (region_params : T.erased_region list) + (type_params : T.ety list) (args : E.operand list) (dest : E.place) : cm_fun + = + (* There are two cases (and this is extremely annoying): + - the function is not box_free + - the function is box_free + See {!eval_box_free} + *) + match fid with + | A.BoxFree -> + (* Degenerate case: box_free *) + eval_box_free config region_params type_params args dest + | _ -> + (* "Normal" case: not box_free *) + (* Evaluate the operands *) + (* let ctx, args_vl = eval_operands config ctx args in *) + let cf_eval_ops = eval_operands config args in + + (* Evaluate the call + * + * Style note: at some point we used {!comp_transmit} to + * transmit the result of {!eval_operands} above down to {!push_vars} + * below, without having to introduce an intermediary function call, + * but it made it less clear where the computed values came from, + * so we reversed the modifications. *) + let cf_eval_call cf (args_vl : V.typed_value list) : m_fun = + (* Push the stack frame: we initialize the frame with the return variable, + and one variable per input argument *) + let cc = push_frame in + + (* Create and push the return variable *) + let ret_vid = V.VarId.zero in + let ret_ty = + get_non_local_function_return_type fid region_params type_params + in + let ret_var = mk_var ret_vid (Some "@return") ret_ty in + let cc = comp cc (push_uninitialized_var ret_var) in + + (* Create and push the input variables *) + let input_vars = + V.VarId.mapi_from1 + (fun id (v : V.typed_value) -> (mk_var id None v.V.ty, v)) + args_vl + in + let cc = comp cc (push_vars input_vars) in + + (* "Execute" the function body. As the functions are assumed, here we call + * custom functions to perform the proper manipulations: we don't have + * access to a body. *) + let cf_eval_body : cm_fun = + match fid with + | A.Replace -> eval_replace_concrete config region_params type_params + | BoxNew -> eval_box_new_concrete config region_params type_params + | BoxDeref -> eval_box_deref_concrete config region_params type_params + | BoxDerefMut -> + eval_box_deref_mut_concrete config region_params type_params + | BoxFree -> + (* Should have been treated above *) raise (Failure "Unreachable") + | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut -> + eval_vec_function_concrete config fid region_params type_params + in + + let cc = comp cc cf_eval_body in + + (* Pop the frame *) + let cc = comp cc (pop_frame_assign config dest) in + + (* Continue *) + cc cf + in + (* Compose and apply *) + comp cf_eval_ops cf_eval_call + +(** Instantiate a function signature, introducing fresh abstraction ids and + region ids. This is mostly used in preparation of function calls, when + evaluating in symbolic mode of course. + + Note: there are no region parameters, because they should be erased. + + **Rk.:** this function is **stateful** and generates fresh abstraction ids + for the region groups. + *) +let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) : + A.inst_fun_sig = + (* Generate fresh abstraction ids and create a substitution from region + * group ids to abstraction ids *) + let rg_abs_ids_bindings = + List.map + (fun rg -> + let abs_id = C.fresh_abstraction_id () in + (rg.T.id, abs_id)) + sg.regions_hierarchy + in + let asubst_map : V.AbstractionId.id T.RegionGroupId.Map.t = + List.fold_left + (fun mp (rg_id, abs_id) -> T.RegionGroupId.Map.add rg_id abs_id mp) + T.RegionGroupId.Map.empty rg_abs_ids_bindings + in + let asubst (rg_id : T.RegionGroupId.id) : V.AbstractionId.id = + T.RegionGroupId.Map.find rg_id asubst_map + in + (* Generate fresh regions and their substitutions *) + let _, rsubst, _ = Subst.fresh_regions_with_substs sg.region_params in + (* Generate the type substitution + * Note that we need the substitution to map the type variables to + * {!rty} types (not {!ety}). In order to do that, we convert the + * type parameters to types with regions. This is possible only + * if those types don't contain any regions. + * This is a current limitation of the analysis: there is still some + * work to do to properly handle full type parametrization. + * *) + let rtype_params = List.map ety_no_regions_to_rty type_params in + let tsubst = + Subst.make_type_subst + (List.map (fun v -> v.T.index) sg.type_params) + rtype_params + in + (* Substitute the signature *) + let inst_sig = Subst.substitute_signature asubst rsubst tsubst sg in + (* Return *) + inst_sig + +(** Helper + + Create abstractions (with no avalues, which have to be inserted afterwards) + from a list of abs region groups. + + [region_can_end]: gives the region groups from which we generate functions + which can end or not. + *) +let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) + (kind : V.abs_kind) (rgl : A.abs_region_group list) + (region_can_end : T.RegionGroupId.id -> bool) : V.abs list = + (* We use a reference to progressively create a map from abstraction ids + * to set of ancestor regions. Note that {!abs_to_ancestors_regions} [abs_id] + * returns the union of: + * - the regions of the ancestors of abs_id + * - the regions of abs_id + *) + let abs_to_ancestors_regions : T.RegionId.Set.t V.AbstractionId.Map.t ref = + ref V.AbstractionId.Map.empty + in + (* Auxiliary function to create one abstraction *) + let create_abs (back_id : T.RegionGroupId.id) (rg : A.abs_region_group) : + V.abs = + let abs_id = rg.T.id in + let original_parents = rg.parents in + let parents = + List.fold_left + (fun s pid -> V.AbstractionId.Set.add pid s) + V.AbstractionId.Set.empty rg.parents + in + let regions = + List.fold_left + (fun s rid -> T.RegionId.Set.add rid s) + T.RegionId.Set.empty rg.regions + in + let ancestors_regions = + List.fold_left + (fun acc parent_id -> + T.RegionId.Set.union acc + (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions)) + T.RegionId.Set.empty rg.parents + in + let ancestors_regions_union_current_regions = + T.RegionId.Set.union ancestors_regions regions + in + let can_end = region_can_end back_id in + abs_to_ancestors_regions := + V.AbstractionId.Map.add abs_id ancestors_regions_union_current_regions + !abs_to_ancestors_regions; + (* Create the abstraction *) + { + V.abs_id; + call_id; + back_id; + kind; + can_end; + parents; + original_parents; + regions; + ancestors_regions; + avalues = []; + } + in + (* Apply *) + T.RegionGroupId.mapi create_abs rgl + +(** Helper. + + Create a list of abstractions from a list of regions groups, and insert + them in the context. + + [region_can_end]: gives the region groups from which we generate functions + which can end or not. + + [compute_abs_avalues]: this function must compute, given an initialized, + empty (i.e., with no avalues) abstraction, compute the avalues which + should be inserted in this abstraction before we insert it in the context. + Note that this function may update the context: it is necessary when + computing borrow projections, for instance. +*) +let create_push_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) + (kind : V.abs_kind) (rgl : A.abs_region_group list) + (region_can_end : T.RegionGroupId.id -> bool) + (compute_abs_avalues : + V.abs -> C.eval_ctx -> C.eval_ctx * V.typed_avalue list) + (ctx : C.eval_ctx) : C.eval_ctx = + (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) + let empty_absl = + create_empty_abstractions_from_abs_region_groups call_id kind rgl + region_can_end + in + + (* Compute and add the avalues to the abstractions, the insert the abstractions + * in the context. *) + let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = + (* Compute the values to insert in the abstraction *) + let ctx, avalues = compute_abs_avalues abs ctx in + (* Add the avalues to the abstraction *) + let abs = { abs with avalues } in + (* Insert the abstraction in the context *) + let ctx = { ctx with env = Abs abs :: ctx.env } in + (* Return *) + ctx + in + List.fold_left insert_abs ctx empty_absl + +(** Evaluate a statement *) +let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = + fun cf ctx -> + (* Debugging *) + log#ldebug + (lazy + ("\n**About to evaluate statement**: [\n" + ^ statement_to_string_with_tab ctx st + ^ "\n]\n\n**Context**:\n" ^ eval_ctx_to_string ctx ^ "\n\n")); + + (* Expand the symbolic values if necessary - we need to do that before + * checking the invariants *) + let cc = greedy_expand_symbolic_values config in + (* Sanity check *) + let cc = comp cc (Inv.cf_check_invariants config) in + + (* Evaluate *) + let cf_eval_st cf : m_fun = + fun ctx -> + match st.content with + | A.Assign (p, rvalue) -> + (* Evaluate the rvalue *) + let cf_eval_rvalue = eval_rvalue config rvalue in + (* Assign *) + let cf_assign cf (res : (V.typed_value, eval_error) result) ctx = + log#ldebug + (lazy + ("about to assign to place: " ^ place_to_string ctx p + ^ "\n- Context:\n" ^ eval_ctx_to_string ctx)); + match res with + | Error EPanic -> cf Panic ctx + | Ok rv -> ( + let expr = assign_to_place config rv p (cf Unit) ctx in + (* Update the synthesized AST - here we store meta-information. + * We do it only in specific cases (it is not always useful, and + * also it can lead to issues - for instance, if we borrow an + * inactivated borrow, we later can't translate it to pure values...) *) + match rvalue with + | E.Use _ + | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut)) + | E.UnaryOp _ | E.BinaryOp _ | E.Discriminant _ | E.Aggregate _ -> + let rp = rvalue_get_place rvalue in + let rp = + match rp with + | Some rp -> Some (S.mk_mplace rp ctx) + | None -> None + in + S.synthesize_assignment (S.mk_mplace p ctx) rv rp expr) + in + + (* Compose and apply *) + comp cf_eval_rvalue cf_assign cf ctx + | A.AssignGlobal { dst; global } -> eval_global config dst global cf ctx + | A.FakeRead p -> + let expand_prim_copy = false in + let cf_prepare cf = + access_rplace_reorganize_and_read config expand_prim_copy Read p cf + in + let cf_continue cf v : m_fun = + fun ctx -> + assert (not (bottom_in_value ctx.ended_regions v)); + cf ctx + in + comp cf_prepare cf_continue (cf Unit) ctx + | A.SetDiscriminant (p, variant_id) -> + set_discriminant config p variant_id cf ctx + | A.Drop p -> drop_value config p (cf Unit) ctx + | A.Assert assertion -> eval_assertion config assertion cf ctx + | A.Call call -> eval_function_call config call cf ctx + | A.Panic -> cf Panic ctx + | A.Return -> cf Return ctx + | A.Break i -> cf (Break i) ctx + | A.Continue i -> cf (Continue i) ctx + | A.Nop -> cf Unit ctx + | A.Sequence (st1, st2) -> + (* Evaluate the first statement *) + let cf_st1 = eval_statement config st1 in + (* Evaluate the sequence *) + let cf_st2 cf res = + match res with + (* Evaluation successful: evaluate the second statement *) + | Unit -> eval_statement config st2 cf + (* Control-flow break: transmit. We enumerate the cases on purpose *) + | Panic | Break _ | Continue _ | Return -> cf res + in + (* Compose and apply *) + comp cf_st1 cf_st2 cf ctx + | A.Loop loop_body -> + (* For now, we don't support loops in symbolic mode *) + assert (config.C.mode = C.ConcreteMode); + (* Continuation for after we evaluate the loop body: depending the result + of doing one loop iteration: + - redoes a loop iteration + - exits the loop + - other... + + We need a specific function because of the {!Continue} case: in case we + continue, we might have to reevaluate the current loop body with the + new context (and repeat this an indefinite number of times). + *) + let rec reeval_loop_body res : m_fun = + match res with + | Return | Panic -> cf res + | Break i -> + (* Break out of the loop by calling the continuation *) + let res = if i = 0 then Unit else Break (i - 1) in + cf res + | Continue 0 -> + (* Re-evaluate the loop body *) + eval_statement config loop_body reeval_loop_body + | Continue i -> + (* Continue to an outer loop *) + cf (Continue (i - 1)) + | Unit -> + (* We can't get there. + * Note that if we decide not to fail here but rather do + * the same thing as for [Continue 0], we could make the + * code slightly simpler: calling {!reeval_loop_body} with + * {!Unit} would account for the first iteration of the loop. + * We prefer to write it this way for consistency and sanity, + * though. *) + raise (Failure "Unreachable") + in + (* Apply *) + eval_statement config loop_body reeval_loop_body ctx + | A.Switch (op, tgts) -> eval_switch config op tgts cf ctx + in + (* Compose and apply *) + comp cc cf_eval_st cf ctx + +and eval_global (config : C.config) (dest : V.VarId.id) + (gid : LA.GlobalDeclId.id) : st_cm_fun = + fun cf ctx -> + let global = C.ctx_lookup_global_decl ctx gid in + let place = { E.var_id = dest; projection = [] } in + match config.mode with + | ConcreteMode -> + (* Treat the evaluation of the global as a call to the global body (without arguments) *) + (eval_local_function_call_concrete config global.body_id [] [] [] place) + cf ctx + | SymbolicMode -> + (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be + * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *) + let sval = + mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty) + in + let cc = + assign_to_place config (mk_typed_value_from_symbolic_value sval) place + in + let e = cc (cf Unit) ctx in + S.synthesize_global_eval gid sval e + +(** Evaluate a switch *) +and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : + st_cm_fun = + fun cf ctx -> + (* We evaluate the operand in two steps: + * first we prepare it, then we check if its value is concrete or + * symbolic. If it is concrete, we can then evaluate the operand + * directly, otherwise we must first expand the value. + * Note that we can't fully evaluate the operand *then* expand the + * value if it is symbolic, because the value may have been move + * (and would thus floating in thin air...)! + * *) + (* Prepare the operand *) + let cf_eval_op cf : m_fun = eval_operand config op cf in + (* Match on the targets *) + let cf_match (cf : st_m_fun) (op_v : V.typed_value) : m_fun = + fun ctx -> + match tgts with + | A.If (st1, st2) -> ( + match op_v.value with + | V.Concrete (V.Bool b) -> + (* Evaluate the if and the branch body *) + let cf_branch cf : m_fun = + (* Branch *) + if b then eval_statement config st1 cf + else eval_statement config st2 cf + in + (* Compose the continuations *) + cf_branch cf ctx + | V.Symbolic sv -> + (* Expand the symbolic boolean, and continue by evaluating + * the branches *) + let cf_true : m_fun = eval_statement config st1 cf in + let cf_false : m_fun = eval_statement config st2 cf in + expand_symbolic_bool config sv + (S.mk_opt_place_from_op op ctx) + cf_true cf_false ctx + | _ -> raise (Failure "Inconsistent state")) + | A.SwitchInt (int_ty, stgts, otherwise) -> ( + match op_v.value with + | V.Concrete (V.Scalar sv) -> + (* Evaluate the branch *) + let cf_eval_branch cf = + (* Sanity check *) + assert (sv.V.int_ty = int_ty); + (* Find the branch *) + match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with + | None -> eval_statement config otherwise cf + | Some (_, tgt) -> eval_statement config tgt cf + in + (* Compose *) + cf_eval_branch cf ctx + | V.Symbolic sv -> + (* Expand the symbolic value and continue by evaluating the + * proper branches *) + let stgts = + List.map + (fun (cv, tgt_st) -> (cv, eval_statement config tgt_st cf)) + stgts + in + (* Several branches may be grouped together: every branch is described + * by a pair (list of values, branch expression). + * In order to do a symbolic evaluation, we make this "flat" by + * de-grouping the branches. *) + let stgts = + List.concat + (List.map + (fun (vl, st) -> List.map (fun v -> (v, st)) vl) + stgts) + in + (* Translate the otherwise branch *) + let otherwise = eval_statement config otherwise cf in + (* Expand and continue *) + expand_symbolic_int config sv + (S.mk_opt_place_from_op op ctx) + int_ty stgts otherwise ctx + | _ -> raise (Failure "Inconsistent state")) + in + (* Compose the continuations *) + comp cf_eval_op cf_match cf ctx + +(** Evaluate a function call (auxiliary helper for [eval_statement]) *) +and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = + (* There are two cases: + - this is a local function, in which case we execute its body + - this is a non-local function, in which case there is a special treatment + *) + match call.func with + | A.Regular fid -> + eval_local_function_call config fid call.region_args call.type_args + call.args call.dest + | A.Assumed fid -> + eval_non_local_function_call config fid call.region_args call.type_args + call.args call.dest + +(** Evaluate a local (i.e., non-assumed) function call in concrete mode *) +and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) + (region_args : T.erased_region list) (type_args : T.ety list) + (args : E.operand list) (dest : E.place) : st_cm_fun = + fun cf ctx -> + assert (region_args = []); + + (* Retrieve the (correctly instantiated) body *) + let def = C.ctx_lookup_fun_decl ctx fid in + (* We can evaluate the function call only if it is not opaque *) + let body = + match def.body with + | None -> + raise + (Failure + ("Can't evaluate a call to an opaque function: " + ^ Print.name_to_string def.name)) + | Some body -> body + in + let tsubst = + Subst.make_type_subst + (List.map (fun v -> v.T.index) def.A.signature.type_params) + type_args + in + let locals, body_st = Subst.fun_body_substitute_in_body tsubst body in + + (* Evaluate the input operands *) + assert (List.length args = body.A.arg_count); + let cc = eval_operands config args in + + (* Push a frame delimiter - we use {!comp_transmit} to transmit the result + * of the operands evaluation from above to the functions afterwards, while + * ignoring it in this function *) + let cc = comp_transmit cc push_frame in + + (* Compute the initial values for the local variables *) + (* 1. Push the return value *) + let ret_var, locals = + match locals with + | ret_ty :: locals -> (ret_ty, locals) + | _ -> raise (Failure "Unreachable") + in + let input_locals, locals = + Collections.List.split_at locals body.A.arg_count + in + + let cc = comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty)) in + + (* 2. Push the input values *) + let cf_push_inputs cf args = + let inputs = List.combine input_locals args in + (* Note that this function checks that the variables and their values + * have the same type (this is important) *) + push_vars inputs cf + in + let cc = comp cc cf_push_inputs in + + (* 3. Push the remaining local variables (initialized as {!Bottom}) *) + let cc = comp cc (push_uninitialized_vars locals) in + + (* Execute the function body *) + let cc = comp cc (eval_function_body config body_st) in + + (* Pop the stack frame and move the return value to its destination *) + let cf_finish cf res = + match res with + | Panic -> cf Panic + | Break _ | Continue _ | Unit -> raise (Failure "Unreachable") + | Return -> + (* Pop the stack frame, retrieve the return value, move it to + * its destination and continue *) + pop_frame_assign config dest (cf Unit) + in + let cc = comp cc cf_finish in + + (* Continue *) + cc cf ctx + +(** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) +and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) + (region_args : T.erased_region list) (type_args : T.ety list) + (args : E.operand list) (dest : E.place) : st_cm_fun = + fun cf ctx -> + (* Retrieve the (correctly instantiated) signature *) + let def = C.ctx_lookup_fun_decl ctx fid in + let sg = def.A.signature in + (* Instantiate the signature and introduce fresh abstraction and region ids + * while doing so *) + let inst_sg = instantiate_fun_sig type_args sg in + (* Sanity check *) + assert (List.length args = List.length def.A.signature.inputs); + (* Evaluate the function call *) + eval_function_call_symbolic_from_inst_sig config (A.Regular fid) inst_sg + region_args type_args args dest cf ctx + +(** Evaluate a function call in symbolic mode by using the function signature. + + This allows us to factorize the evaluation of local and non-local function + calls in symbolic mode: only their signatures matter. + *) +and eval_function_call_symbolic_from_inst_sig (config : C.config) + (fid : A.fun_id) (inst_sg : A.inst_fun_sig) + (region_args : T.erased_region list) (type_args : T.ety list) + (args : E.operand list) (dest : E.place) : st_cm_fun = + fun cf ctx -> + assert (region_args = []); + (* Generate a fresh symbolic value for the return value *) + let ret_sv_ty = inst_sg.A.output in + let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in + let ret_value = mk_typed_value_from_symbolic_value ret_spc in + let ret_av regions = + mk_aproj_loans_value_from_symbolic_value regions ret_spc + in + let args_places = List.map (fun p -> S.mk_opt_place_from_op p ctx) args in + let dest_place = Some (S.mk_mplace dest ctx) in + + (* Evaluate the input operands *) + let cc = eval_operands config args in + + (* Generate the abstractions and insert them in the context *) + let abs_ids = List.map (fun rg -> rg.T.id) inst_sg.regions_hierarchy in + let cf_call cf (args : V.typed_value list) : m_fun = + fun ctx -> + let args_with_rtypes = List.combine args inst_sg.A.inputs in + + (* Check the type of the input arguments *) + assert ( + List.for_all + (fun ((arg, rty) : V.typed_value * T.rty) -> + arg.V.ty = Subst.erase_regions rty) + args_with_rtypes); + (* Check that the input arguments don't contain symbolic values that can't + * be fed to functions (i.e., symbolic values output from function return + * values and which contain borrows of borrows can't be used as function + * inputs *) + assert ( + List.for_all + (fun arg -> + not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) + args); + + (* Initialize the abstractions and push them in the context. + * First, we define the function which, given an initialized, empty + * abstraction, computes the avalues which should be inserted inside. + *) + let compute_abs_avalues (abs : V.abs) (ctx : C.eval_ctx) : + C.eval_ctx * V.typed_avalue list = + (* Project over the input values *) + let ctx, args_projs = + List.fold_left_map + (fun ctx (arg, arg_rty) -> + apply_proj_borrows_on_input_value config ctx abs.regions + abs.ancestors_regions arg arg_rty) + ctx args_with_rtypes + in + (* Group the input and output values *) + (ctx, List.append args_projs [ ret_av abs.regions ]) + in + (* Actually initialize and insert the abstractions *) + let call_id = C.fresh_fun_call_id () in + let region_can_end _ = true in + let ctx = + create_push_abstractions_from_abs_region_groups call_id V.FunCall + inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx + in + + (* Apply the continuation *) + let expr = cf ctx in + + (* Synthesize the symbolic AST *) + S.synthesize_regular_function_call fid call_id abs_ids type_args args + args_places ret_spc dest_place expr + in + let cc = comp cc cf_call in + + (* Move the return value to its destination *) + let cc = comp cc (assign_to_place config ret_value dest) in + + (* End the abstractions which don't contain loans and don't have parent + * abstractions. + * We do the general, nested borrows case here: we end abstractions, then + * retry (because then we might end their children abstractions) + *) + let abs_ids = ref abs_ids in + let rec end_abs_with_no_loans cf : m_fun = + fun ctx -> + (* Find the abstractions which don't contain loans *) + let no_loans_abs, with_loans_abs = + List.partition + (fun abs_id -> + (* Lookup the abstraction *) + let abs = C.ctx_lookup_abs ctx abs_id in + (* Check if it has parents *) + V.AbstractionId.Set.is_empty abs.parents + (* Check if it contains non-ignored loans *) + && Option.is_none + (InterpreterBorrowsCore + .get_first_non_ignored_aloan_in_abstraction abs)) + !abs_ids + in + (* Check if there are abstractions to end *) + if no_loans_abs <> [] then ( + (* Update the reference to the list of asbtraction ids, for the recursive calls *) + abs_ids := with_loans_abs; + (* End the abstractions which can be ended *) + let no_loans_abs = V.AbstractionId.Set.of_list no_loans_abs in + let cc = InterpreterBorrows.end_abstractions config [] no_loans_abs in + (* Recursive call *) + let cc = comp cc end_abs_with_no_loans in + (* Continue *) + cc cf ctx) + else (* No abstractions to end: continue *) + cf ctx + in + (* Try to end the abstractions with no loans if: + * - the option is enabled + * - the function returns unit + * (see the documentation of {!config} for more information) + *) + let cc = + if config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output + then comp cc end_abs_with_no_loans + else cc + in + + (* Continue - note that we do as if the function call has been successful, + * by giving {!Unit} to the continuation, because we place us in the case + * where we haven't panicked. Of course, the translation needs to take the + * panic case into account... *) + cc (cf Unit) ctx + +(** Evaluate a non-local function call in symbolic mode *) +and eval_non_local_function_call_symbolic (config : C.config) + (fid : A.assumed_fun_id) (region_args : T.erased_region list) + (type_args : T.ety list) (args : E.operand list) (dest : E.place) : + st_cm_fun = + fun cf ctx -> + (* Sanity check: make sure the type parameters don't contain regions - + * this is a current limitation of our synthesis *) + assert ( + List.for_all + (fun ty -> not (ty_has_borrows ctx.type_context.type_infos ty)) + type_args); + + (* There are two cases (and this is extremely annoying): + - the function is not box_free + - the function is box_free + See {!eval_box_free} + *) + match fid with + | A.BoxFree -> + (* Degenerate case: box_free - note that this is not really a function + * call: no need to call a "synthesize_..." function *) + eval_box_free config region_args type_args args dest (cf Unit) ctx + | _ -> + (* "Normal" case: not box_free *) + (* In symbolic mode, the behaviour of a function call is completely defined + * by the signature of the function: we thus simply generate correctly + * instantiated signatures, and delegate the work to an auxiliary function *) + let inst_sig = + match fid with + | A.BoxFree -> + (* should have been treated above *) + raise (Failure "Unreachable") + | _ -> instantiate_fun_sig type_args (Assumed.get_assumed_sig fid) + in + + (* Evaluate the function call *) + eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig + region_args type_args args dest cf ctx + +(** Evaluate a non-local (i.e, assumed) function call such as [Box::deref] + (auxiliary helper for [eval_statement]) *) +and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id) + (region_args : T.erased_region list) (type_args : T.ety list) + (args : E.operand list) (dest : E.place) : st_cm_fun = + fun cf ctx -> + (* Debug *) + log#ldebug + (lazy + (let type_args = + "[" ^ String.concat ", " (List.map (ety_to_string ctx) type_args) ^ "]" + in + let args = + "[" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "]" + in + let dest = place_to_string ctx dest in + "eval_non_local_function_call:\n- fid:" ^ A.show_assumed_fun_id fid + ^ "\n- type_args: " ^ type_args ^ "\n- args: " ^ args ^ "\n- dest: " + ^ dest)); + + match config.mode with + | C.ConcreteMode -> + eval_non_local_function_call_concrete config fid region_args type_args + args dest (cf Unit) ctx + | C.SymbolicMode -> + eval_non_local_function_call_symbolic config fid region_args type_args + args dest cf ctx + +(** Evaluate a local (i.e, not assumed) function call (auxiliary helper for + [eval_statement]) *) +and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id) + (region_args : T.erased_region list) (type_args : T.ety list) + (args : E.operand list) (dest : E.place) : st_cm_fun = + match config.mode with + | ConcreteMode -> + eval_local_function_call_concrete config fid region_args type_args args + dest + | SymbolicMode -> + eval_local_function_call_symbolic config fid region_args type_args args + dest + +(** Evaluate a statement seen as a function body (auxiliary helper for + [eval_statement]) *) +and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun = + fun cf ctx -> + let cc = eval_statement config body in + let cf_finish cf res = + (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we + * delegate the check to the caller. *) + (* Expand the symbolic values if necessary - we need to do that before + * checking the invariants *) + let cc = greedy_expand_symbolic_values config in + (* Sanity check *) + let cc = comp_check_ctx cc (Inv.check_invariants config) in + (* Continue *) + cc (cf res) + in + (* Compose and continue *) + comp cc cf_finish cf ctx |