module T = Types module PV = PrimitiveValues 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 Utils open Cps open InterpreterUtils open InterpreterProjectors open InterpreterExpansion open InterpreterPaths open InterpreterExpressions module PCtx = Print.EvalCtxLlbcAst (** 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)); (* Note that we use [Write], not [Move]: we allow to drop values *below* borrows *) let access = Write in (* First make sure we can access the place, by ending loans or expanding * symbolic values along the path, for instance *) let cc = update_ctx_along_read_place config access p in (* Prepare the place (by ending the outer loans *at* the place). *) let cc = comp cc (prepare_lplace config 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 it may contain *) let mv = InterpreterPaths.read_place access p ctx in let dummy_id = C.fresh_dummy_var_id () in let ctx = C.ctx_push_dummy_var ctx dummy_id mv in (* Update the destination to ⊥ *) let nv = { v with value = V.Bottom } in let ctx = write_place access 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 cc replace cf ctx (** Push a dummy variable to the environment *) let push_dummy_var (vid : C.DummyVarId.id) (v : V.typed_value) : cm_fun = fun cf ctx -> let ctx = C.ctx_push_dummy_var ctx vid v in cf ctx (** Remove a dummy variable from the environment *) let remove_dummy_var (vid : C.DummyVarId.id) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> let ctx, v = C.ctx_remove_dummy_var ctx vid 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 rvalue_vid = C.fresh_dummy_var_id () in let cc = push_dummy_var rvalue_vid rv in (* Prepare the destination *) let cc = comp cc (prepare_lplace config p) in (* Retrieve the rvalue from the dummy variable *) let cc = comp cc (fun cf _lv -> remove_dummy_var rvalue_vid 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 = InterpreterPaths.read_place Write p ctx in let dest_vid = C.fresh_dummy_var_id () in let ctx = C.ctx_push_dummy_var ctx dest_vid 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 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 | Literal (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.Literal PV.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 | Literal (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.Literal PV.Bool); (* We continue the execution as if the test had succeeded, and thus * perform the symbolic expansion: sv ~~> true. * We will of course synthesize an assertion in the generated code * (see below). *) let ctx = apply_symbolic_expansion_non_borrow config sv (V.SeLiteral (PV.Bool true)) ctx in (* Continue *) let expr = cf Unit ctx in (* Add the synthesized assertion *) S.synthesize_assertion ctx v expr | _ -> 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 cc = comp cc (prepare_lplace config 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), generics), 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 def_id (Some variant_id) generics | T.Assumed T.Option -> assert (generics.regions = []); compute_expanded_bottom_option_value variant_id (Collections.List.to_cons_nil generics.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), generics), V.Bottom -> let bottom_v = match type_id with | T.AdtId def_id -> compute_expanded_bottom_adt_value ctx def_id (Some variant_id) generics | T.Assumed T.Option -> assert (generics.regions = []); compute_expanded_bottom_option_value variant_id (Collections.List.to_cons_nil generics.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.Literal _ | 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 an assumed function. *) let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id) (generics : T.egeneric_args) : T.ety = assert (generics.trait_refs = []); (* [Box::free] has a special treatment *) match fid with | A.BoxFree -> assert (generics.regions = []); assert (List.length generics.types = 1); assert (generics.const_generics = []); mk_unit_ty | _ -> (* Retrieve the function's signature *) let sg = Assumed.get_assumed_sig fid in (* Instantiate the return type *) (* There shouldn't be any reference to Self *) let tr_self : T.erased_region T.trait_instance_id = T.UnknownTrait __FUNCTION__ in let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = Subst.make_esubst_from_generics sg.generics generics tr_self in let ty = Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self sg.output in Assoc.ctx_normalize_ety ctx ty let move_return_value (config : C.config) (pop_return_value : bool) (cf : V.typed_value option -> m_fun) : m_fun = fun ctx -> if pop_return_value then let ret_vid = E.VarId.zero in let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in cc (fun v ctx -> cf (Some v) ctx) ctx else cf None ctx let pop_frame (config : C.config) (pop_return_value : bool) (cf : V.typed_value option -> m_fun) : m_fun = fun ctx -> (* Debug *) log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ctx)); (* List the local variables, but the return variable *) let ret_vid = E.VarId.zero in let rec list_locals env = match env with | [] -> raise (Failure "Inconsistent environment") | C.Abs _ :: env -> list_locals env | C.Var (DummyBinder _, _) :: env -> list_locals env | C.Var (VarBinder var, _) :: env -> let locals = list_locals env in if var.index <> ret_vid then var.index :: locals else locals | C.Frame :: _ -> [] in let locals : E.VarId.id list = list_locals ctx.env in (* Debug *) log#ldebug (lazy ("pop_frame: locals in which to drop the outer loans: [" ^ String.concat "," (List.map E.VarId.to_string locals) ^ "]")); (* Move the return value out of the return variable *) let cc = move_return_value config pop_return_value in (* Sanity check *) let cc = comp_check_value cc (fun ret_value ctx -> match ret_value with | None -> () | Some ret_value -> 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 option) : m_fun = (* Drop the loans *) let locals = List.rev locals in let cf_drop = List.fold_left (fun cf lid -> drop_outer_loans_at_lplace config (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 ("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 -> let vid = C.fresh_dummy_var_id () in C.Var (C.DummyBinder vid, v) :: pop env | C.Frame :: env -> (* Stop here *) env in let cf_pop cf (ret_value : V.typed_value option) : 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 = pop_frame config true in let cf_assign cf ret_value : m_fun = assign_to_place config (Option.get ret_value) dest cf in comp cf_pop cf_assign (** Auxiliary function - see {!eval_assumed_function_call} *) let eval_replace_concrete (_config : C.config) (_generics : T.egeneric_args) : cm_fun = fun _cf _ctx -> raise Unimplemented (** Auxiliary function - see {!eval_assumed_function_call} *) let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) : cm_fun = fun cf ctx -> (* Check and retrieve the arguments *) match (generics.regions, generics.types, generics.const_generics, ctx.env) with | ( [], [ boxed_ty ], [], Var (VarBinder 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 generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in let box_ty = T.Adt (T.Assumed T.Box, generics) 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 E.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_assumed_function_call} *) let eval_box_deref_mut_or_shared_concrete (config : C.config) (generics : T.egeneric_args) (is_mut : bool) : cm_fun = fun cf ctx -> (* Check the arguments *) match (generics.regions, generics.types, generics.const_generics, ctx.env) with | ( [], [ boxed_ty ], [], Var (VarBinder input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) -> (* Required type checking. We must have: - input_value.ty = & (mut) Box - 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.RvRef (p, borrow_kind) in let cf_borrow = eval_rvalue_not_global 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 E.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_assumed_function_call} *) let eval_box_deref_concrete (config : C.config) (generics : T.egeneric_args) : cm_fun = let is_mut = false in eval_box_deref_mut_or_shared_concrete config generics is_mut (** Auxiliary function - see {!eval_assumed_function_call} *) let eval_box_deref_mut_concrete (config : C.config) (generics : T.egeneric_args) : cm_fun = let is_mut = true in eval_box_deref_mut_or_shared_concrete config generics is_mut (** Auxiliary function - see {!eval_assumed_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) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : cm_fun = fun cf ctx -> match (generics.regions, generics.types, generics.const_generics, args) with | [], [ boxed_ty ], [], [ E.Move input_box_place ] -> (* Required type checking *) let input_box = InterpreterPaths.read_place 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_assumed_function_call} *) let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) (_generics : T.egeneric_args) : cm_fun = fun _cf _ctx -> raise Unimplemented (** Evaluate a non-local function call in concrete mode *) let eval_assumed_function_call_concrete (config : C.config) (fid : A.assumed_fun_id) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : cm_fun = (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) assert (generics.const_generics = []); (* 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 generics 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 = fun ctx -> (* 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 = E.VarId.zero in let ret_ty = get_assumed_function_return_type ctx fid generics 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 = E.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 generics | BoxNew -> eval_box_new_concrete config generics | BoxDeref -> eval_box_deref_concrete config generics | BoxDerefMut -> eval_box_deref_mut_concrete config generics | BoxFree -> (* Should have been treated above *) raise (Failure "Unreachable") | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut -> eval_vec_function_concrete config fid generics | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut | SliceIndexShared | SliceIndexMut | SliceSubsliceShared | SliceSubsliceMut | SliceLen -> raise (Failure "Unimplemented") 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 ctx in (* Compose and apply *) comp cf_eval_ops cf_eval_call let instantiate_fun_sig (ctx : C.eval_ctx) (generics : T.egeneric_args) (tr_self : T.rtrait_instance_id) (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.generics.regions 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 generics.types in let tsubst = Subst.make_type_subst_from_vars sg.generics.types rtype_params in let cgsubst = Subst.make_const_generic_subst_from_vars sg.generics.const_generics generics.const_generics in (* TODO: something annoying with the trait ref subst: we need to use region types, but the arguments use erased regions. For now we use the fact that no regions should appear inside. In the future: we should merge ety and rty. *) let trait_refs = List.map TypesUtils.etrait_ref_no_regions_to_gr_trait_ref generics.trait_refs in let tr_subst = Subst.make_trait_subst_from_clauses sg.generics.trait_clauses trait_refs in (* Substitute the signature *) let inst_sig = Assoc.ctx_subst_norm_signature ctx asubst rsubst tsubst cgsubst tr_subst tr_self 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 (kind : T.RegionGroupId.id -> 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 (rg_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 rg_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; kind = kind rg_id; can_end; parents; original_parents; regions; ancestors_regions; avalues = []; } in (* Apply *) T.RegionGroupId.mapi create_abs rgl let create_push_abstractions_from_abs_region_groups (kind : T.RegionGroupId.id -> 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 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 in (* Evaluate *) let cf_eval_st cf : m_fun = fun ctx -> match st.content with | A.Assign (p, rvalue) -> ( (* We handle global assignments separately *) match rvalue with | E.Global gid -> (* Evaluate the global *) eval_global config p gid cf ctx | _ -> (* Evaluate the rvalue *) let cf_eval_rvalue = eval_rvalue_not_global 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 a * reserved borrow, we later can't translate it to pure values...) *) match rvalue with | E.Global _ -> raise (Failure "Unreachable") | E.Use _ | E.RvRef (_, (E.Shared | E.Mut | E.TwoPhaseMut | E.Shallow)) | 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 ctx (S.mk_mplace p ctx) rv rp expr ) in (* Compose and apply *) comp cf_eval_rvalue cf_assign cf ctx) | A.FakeRead p -> eval_fake_read config p (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 | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> cf res in (* Compose and apply *) comp cf_st1 cf_st2 cf ctx | A.Loop loop_body -> InterpreterLoops.eval_loop config (eval_statement config loop_body) cf ctx | A.Switch switch -> eval_switch config switch cf ctx in (* Compose and apply *) comp cc cf_eval_st cf ctx and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id) : st_cm_fun = fun cf ctx -> let global = C.ctx_lookup_global_decl ctx gid in match config.mode with | ConcreteMode -> (* Treat the evaluation of the global as a call to the global body (without arguments) *) let generics = TypesUtils.mk_empty_generic_args in (eval_transparent_function_call_concrete config global.body_id generics [] dest) 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) dest in let e = cc (cf Unit) ctx in S.synthesize_global_eval gid sval e (** Evaluate a switch *) and eval_switch (config : C.config) (switch : A.switch) : 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...)! * *) (* Match on the targets *) let cf_match : st_cm_fun = fun cf ctx -> match switch with | A.If (op, st1, st2) -> (* Evaluate the operand *) let cf_eval_op = eval_operand config op in (* Switch on the value *) let cf_if (cf : st_m_fun) (op_v : V.typed_value) : m_fun = fun ctx -> match op_v.value with | V.Literal (PV.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 : st_cm_fun = eval_statement config st1 in let cf_false : st_cm_fun = eval_statement config st2 in expand_symbolic_bool config sv (S.mk_opt_place_from_op op ctx) cf_true cf_false cf ctx | _ -> raise (Failure "Inconsistent state") in (* Compose *) comp cf_eval_op cf_if cf ctx | A.SwitchInt (op, int_ty, stgts, otherwise) -> (* Evaluate the operand *) let cf_eval_op = eval_operand config op in (* Switch on the value *) let cf_switch (cf : st_m_fun) (op_v : V.typed_value) : m_fun = fun ctx -> match op_v.value with | V.Literal (PV.Scalar sv) -> (* Evaluate the branch *) let cf_eval_branch cf = (* Sanity check *) assert (sv.PV.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)) 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 in (* Expand and continue *) expand_symbolic_int config sv (S.mk_opt_place_from_op op ctx) int_ty stgts otherwise cf ctx | _ -> raise (Failure "Inconsistent state") in (* Compose *) comp cf_eval_op cf_switch cf ctx | A.Match (p, stgts, otherwise) -> (* Access the place *) let access = Read in let expand_prim_copy = false in let cf_read_p cf : m_fun = access_rplace_reorganize_and_read config expand_prim_copy access p cf in (* Match on the value *) let cf_match (cf : st_m_fun) (p_v : V.typed_value) : m_fun = fun ctx -> (* The value may be shared: we need to ignore the shared loans to read the value itself *) let p_v = value_strip_shared_loans p_v in (* Match *) match p_v.value with | V.Adt adt -> ( (* Evaluate the discriminant *) let dv = Option.get adt.variant_id in (* Find the branch, evaluate and continue *) match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with | None -> eval_statement config otherwise cf ctx | Some (_, tgt) -> eval_statement config tgt cf ctx) | V.Symbolic sv -> (* Expand the symbolic value - may lead to branching *) let cf_expand = 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 *) cf_expand (eval_switch config switch) cf ctx | _ -> raise (Failure "Inconsistent state") in (* Compose *) comp cf_read_p cf_match cf ctx in (* Compose the continuations *) 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 several cases: - this is a local function, in which case we execute its body - this is an assumed function, in which case there is a special treatment - this is a trait method *) match call.func with | A.FunId (A.Regular fid) -> eval_transparent_function_call config fid call.generics call.args call.dest | A.FunId (A.Assumed fid) -> eval_assumed_function_call config fid call.generics call.args call.dest | A.TraitMethod _ -> raise (Failure "Unimplemented") (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) and eval_transparent_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : st_cm_fun = (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) assert (generics.const_generics = []); fun cf ctx -> (* 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 (* TODO: we need to normalize the types if we want to correctly support traits *) assert (generics.trait_refs = []); (* There shouldn't be any reference to Self *) let tr_self = T.UnknownTrait __FUNCTION__ in let subst = Subst.make_esubst_from_generics def.A.signature.generics generics tr_self in let locals, body_st = Subst.fun_body_substitute_in_body subst 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 | Return -> (* Pop the stack frame, retrieve the return value, move it to * its destination and continue *) pop_frame_assign config dest (cf Unit) | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> raise (Failure "Unreachable") 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_transparent_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) (generics : T.egeneric_args) (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 *) (* There shouldn't be any reference to Self *) let tr_self = T.UnknownTrait __FUNCTION__ in let inst_sg = instantiate_fun_sig ctx generics tr_self 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 generics 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) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* 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 (fun rg_id -> V.FunCall (call_id, rg_id)) 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 ctx abs_ids generics 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_assumed_function_call_symbolic (config : C.config) (fid : A.assumed_fun_id) (generics : T.egeneric_args) (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)) generics.types); (* 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 generics 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") | _ -> (* There shouldn't be any reference to Self *) let tr_self = T.UnknownTrait __FUNCTION__ in instantiate_fun_sig ctx generics tr_self (Assumed.get_assumed_sig fid) in (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig generics args dest cf ctx (** Evaluate a non-local (i.e, assumed) function call such as [Box::deref] (auxiliary helper for [eval_statement]) *) and eval_assumed_function_call (config : C.config) (fid : A.assumed_fun_id) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* Debug *) log#ldebug (lazy (let generics = PCtx.egeneric_args_to_string ctx generics in let args = "[" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "]" in let dest = place_to_string ctx dest in "eval_assumed_function_call:\n- fid:" ^ A.show_assumed_fun_id fid ^ "\n- generics: " ^ generics ^ "\n- args: " ^ args ^ "\n- dest: " ^ dest)); match config.mode with | C.ConcreteMode -> eval_assumed_function_call_concrete config fid generics args dest (cf Unit) ctx | C.SymbolicMode -> eval_assumed_function_call_symbolic config fid generics args dest cf ctx (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for [eval_statement]) *) and eval_transparent_function_call (config : C.config) (fid : A.FunDeclId.id) (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) : st_cm_fun = match config.mode with | ConcreteMode -> eval_transparent_function_call_concrete config fid generics args dest | SymbolicMode -> eval_transparent_function_call_symbolic config fid generics args dest (** Evaluate a statement seen as a function body *) 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 in (* Continue *) cc (cf res) in (* Compose and continue *) comp cc cf_finish cf ctx