open Types open TypesUtils open Values open ValuesUtils open Expressions open Contexts open LlbcAst open Cps open InterpreterUtils open InterpreterProjectors open InterpreterExpansion open InterpreterPaths open InterpreterExpressions open Errors module Subst = Substitute module S = SynthesizeSymbolic (** 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 : config) (span : Meta.span) (p : place) : cm_fun = fun ctx -> log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n" ^ eval_ctx_to_string ~span:(Some span) 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 ctx, cc = update_ctx_along_read_place config span access p ctx in (* Prepare the place (by ending the outer loans *at* the place). *) let v, ctx, cc = comp2 cc (prepare_lplace config span p ctx) in (* Replace the value with {!Bottom} *) let 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 span access p ctx in let dummy_id = fresh_dummy_var_id () in let ctx = ctx_push_dummy_var ctx dummy_id mv in (* Update the destination to ⊥ *) let nv = { v with value = VBottom } in let ctx = write_place span access p nv ctx in log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n" ^ eval_ctx_to_string ~span:(Some span) ctx)); ctx in (* Compose and apply *) (ctx, cc) (** Push a dummy variable to the environment *) let push_dummy_var (vid : DummyVarId.id) (v : typed_value) (ctx : eval_ctx) : eval_ctx = ctx_push_dummy_var ctx vid v (** Remove a dummy variable from the environment *) let remove_dummy_var (span : Meta.span) (vid : DummyVarId.id) (ctx : eval_ctx) : typed_value * eval_ctx = let ctx, v = ctx_remove_dummy_var span ctx vid in (v, ctx) (** Push an uninitialized variable to the environment *) let push_uninitialized_var (span : Meta.span) (var : var) (ctx : eval_ctx) : eval_ctx = ctx_push_uninitialized_var span ctx var (** Push a list of uninitialized variables to the environment *) let push_uninitialized_vars (span : Meta.span) (vars : var list) (ctx : eval_ctx) : eval_ctx = ctx_push_uninitialized_vars span ctx vars (** Push a variable to the environment *) let push_var (span : Meta.span) (var : var) (v : typed_value) (ctx : eval_ctx) : eval_ctx = ctx_push_var span ctx var v (** Push a list of variables to the environment *) let push_vars (span : Meta.span) (vars : (var * typed_value) list) (ctx : eval_ctx) : eval_ctx = ctx_push_vars span ctx vars (** 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 : config) (span : Meta.span) (rv : typed_value) (p : place) : cm_fun = fun ctx -> log#ldebug (lazy ("assign_to_place:" ^ "\n- rv: " ^ typed_value_to_string ~span:(Some span) ctx rv ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Initial context:\n" ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Push the rvalue to a dummy variable, for bookkeeping *) let rvalue_vid = fresh_dummy_var_id () in let ctx = push_dummy_var rvalue_vid rv ctx in (* Prepare the destination *) let _, ctx, cc = prepare_lplace config span p ctx in (* Retrieve the rvalue from the dummy variable *) let rv, ctx = remove_dummy_var span rvalue_vid ctx in (* Move the value at destination (that we will overwrite) to a dummy variable to preserve the borrows *) let mv = InterpreterPaths.read_place span Write p ctx in let dest_vid = fresh_dummy_var_id () in let ctx = ctx_push_dummy_var ctx dest_vid mv in (* Write to the destination *) (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) exec_assert __FILE__ __LINE__ (not (bottom_in_value ctx.ended_regions rv)) span "The value to move contains bottom"; (* Update the destination *) let ctx = write_place span Write p rv ctx in (* Debug *) log#ldebug (lazy ("assign_to_place:" ^ "\n- rv: " ^ typed_value_to_string ~span:(Some span) ctx rv ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n" ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Return *) (ctx, cc) (** Evaluate an assertion, when the scrutinee is not symbolic *) let eval_assertion_concrete (config : config) (span : Meta.span) (assertion : assertion) : st_cm_fun = fun ctx -> (* There won't be any symbolic expansions: fully evaluate the operand *) let v, ctx, eval_op = eval_operand config span assertion.cond ctx in let st = match v.value with | VLiteral (VBool b) -> (* Branch *) if b = assertion.expected then Unit else Panic | _ -> craise __FILE__ __LINE__ span ("Expected a boolean, got: " ^ typed_value_to_string ~span:(Some span) ctx v) in (* Compose and apply *) ((ctx, st), eval_op) (** 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 : config) (span : Meta.span) (assertion : assertion) : st_cm_fun = fun ctx -> (* Evaluate the operand *) let v, ctx, cf_eval_op = eval_operand config span assertion.cond ctx in (* Evaluate the assertion *) sanity_check __FILE__ __LINE__ (v.ty = TLiteral TBool) span; let st, cf_eval_assert = (* 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 | VLiteral (VBool _) -> (* Delegate to the concrete evaluation function *) eval_assertion_concrete config span assertion ctx | VSymbolic sv -> sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) span; sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral TBool) span; (* 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 span sv ctx (SeLiteral (VBool true)) in (* Add the synthesized assertion *) ((ctx, Unit), S.synthesize_assertion ctx v) | _ -> craise __FILE__ __LINE__ span ("Expected a boolean, got: " ^ typed_value_to_string ~span:(Some span) ctx v) in (* Compose and apply *) (st, cc_comp cf_eval_op cf_eval_assert) (** 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 {!Bottom} - this happens when initializing ADT values), in which case we replace the value with a variant with all its fields set to {!Bottom}. For instance, something like: [Cons Bottom Bottom]. *) let set_discriminant (config : config) (span : Meta.span) (p : place) (variant_id : VariantId.id) : st_cm_fun = fun ctx -> log#ldebug (lazy ("set_discriminant:" ^ "\n- p: " ^ place_to_string ctx p ^ "\n- variant id: " ^ VariantId.to_string variant_id ^ "\n- initial context:\n" ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Access the value *) let access = Write in let ctx, cc = update_ctx_along_read_place config span access p ctx in let v, ctx, cc = comp2 cc (prepare_lplace config span p ctx) in (* Update the value *) match (v.ty, v.value) with | TAdt ((TAdtId _ as type_id), generics), VAdt 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 -> craise __FILE__ __LINE__ span "Found a struct value while expecting an enum" | Some variant_id' -> if variant_id' = variant_id then (* Nothing to do *) ((ctx, Unit), cc) else (* Replace the value *) let bottom_v = match type_id with | TAdtId def_id -> compute_expanded_bottom_adt_value span ctx def_id (Some variant_id) generics | _ -> craise __FILE__ __LINE__ span "Unreachable" in let ctx, cc = comp cc (assign_to_place config span bottom_v p ctx) in ((ctx, Unit), cc)) | TAdt ((TAdtId _ as type_id), generics), VBottom -> let bottom_v = match type_id with | TAdtId def_id -> compute_expanded_bottom_adt_value span ctx def_id (Some variant_id) generics | _ -> craise __FILE__ __LINE__ span "Unreachable" in let ctx, cc = comp cc (assign_to_place config span bottom_v p ctx) in ((ctx, Unit), cc) | _, VSymbolic _ -> sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) span; (* 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. *) craise __FILE__ __LINE__ span "Unexpected value" | _, (VAdt _ | VBottom) -> craise __FILE__ __LINE__ span "Inconsistent state" | _, (VLiteral _ | VBorrow _ | VLoan _) -> craise __FILE__ __LINE__ span "Unexpected value" (** Push a frame delimiter in the context's environment *) let ctx_push_frame (ctx : eval_ctx) : eval_ctx = { ctx with env = EFrame :: ctx.env } (** Push a frame delimiter in the context's environment *) let push_frame (ctx : eval_ctx) : eval_ctx = 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 (span : Meta.span) (ctx : eval_ctx) (fid : assumed_fun_id) (generics : generic_args) : ety = sanity_check __FILE__ __LINE__ (generics.trait_refs = []) span; (* [Box::free] has a special treatment *) match fid with | BoxFree -> sanity_check __FILE__ __LINE__ (generics.regions = []) span; sanity_check __FILE__ __LINE__ (List.length generics.types = 1) span; sanity_check __FILE__ __LINE__ (generics.const_generics = []) span; mk_unit_ty | _ -> (* Retrieve the function's signature *) let sg = Assumed.get_assumed_fun_sig fid in (* Instantiate the return type *) (* There shouldn't be any reference to Self *) let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in let generics = Subst.generic_args_erase_regions generics in let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = Subst.make_subst_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 AssociatedTypes.ctx_normalize_erase_ty span ctx ty let move_return_value (config : config) (span : Meta.span) (pop_return_value : bool) (ctx : eval_ctx) : typed_value option * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression) = if pop_return_value then let ret_vid = VarId.zero in let v, ctx, cc = eval_operand config span (Move (mk_place_from_var_id ret_vid)) ctx in (Some v, ctx, cc) else (None, ctx, fun e -> e) let pop_frame (config : config) (span : Meta.span) (pop_return_value : bool) (ctx : eval_ctx) : typed_value option * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression) = (* Debug *) log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~span:(Some span) ctx)); (* List the local variables, but the return variable *) let ret_vid = VarId.zero in let rec list_locals env = match env with | [] -> craise __FILE__ __LINE__ span "Inconsistent environment" | EAbs _ :: env -> list_locals env | EBinding (BDummy _, _) :: env -> list_locals env | EBinding (BVar var, _) :: env -> let locals = list_locals env in if var.index <> ret_vid then var.index :: locals else locals | EFrame :: _ -> [] in let locals : 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 VarId.to_string locals) ^ "]")); (* Move the return value out of the return variable *) let v, ctx, cc = move_return_value config span pop_return_value ctx in let _ = match v with | None -> () | Some ret_value -> sanity_check __FILE__ __LINE__ (not (bottom_in_value ctx.ended_regions ret_value)) span in (* Drop the outer *loans* we find in the local variables *) let ctx, cc = comp cc ((* Drop the loans *) let locals = List.rev locals in fold_left_apply_continuation (fun lid ctx -> drop_outer_loans_at_lplace config span (mk_place_from_var_id lid) ctx) locals ctx) in (* Debug *) log#ldebug (lazy ("pop_frame: after dropping outer loans in local variables:\n" ^ eval_ctx_to_string ~span:(Some span) ctx)); (* 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 | [] -> craise __FILE__ __LINE__ span "Inconsistent environment" | EAbs abs :: env -> EAbs abs :: pop env | EBinding (_, v) :: env -> let vid = fresh_dummy_var_id () in EBinding (BDummy vid, v) :: pop env | EFrame :: env -> (* Stop here *) env in let env = pop ctx.env in let ctx = { ctx with env } in (* Return *) (v, ctx, cc) (** Pop the current frame and assign the returned value to its destination. *) let pop_frame_assign (config : config) (span : Meta.span) (dest : place) : cm_fun = fun ctx -> let v, ctx, cc = pop_frame config span true ctx in comp cc (assign_to_place config span (Option.get v) dest ctx) (** Auxiliary function - see {!eval_assumed_function_call} *) let eval_box_new_concrete (config : config) (span : Meta.span) (generics : generic_args) : cm_fun = fun ctx -> (* Check and retrieve the arguments *) match (generics.regions, generics.types, generics.const_generics, ctx.env) with | ( [], [ boxed_ty ], [], EBinding (BVar input_var, input_value) :: EBinding (_ret_var, _) :: EFrame :: _ ) -> (* Required type checking *) cassert __FILE__ __LINE__ (input_value.ty = boxed_ty) span "The input given to Box::new doesn't have the proper type"; (* Move the input value *) let v, ctx, cc = eval_operand config span (Move (mk_place_from_var_id input_var.index)) ctx in (* Create the new box *) (* Create the box value *) let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in let box_ty = TAdt (TAssumed TBox, generics) in let box_v = VAdt { variant_id = None; field_values = [ v ] } in let box_v = mk_typed_value span box_ty box_v in (* Move this value to the return variable *) let dest = mk_place_from_var_id VarId.zero in comp cc (assign_to_place config span box_v dest ctx) | _ -> craise __FILE__ __LINE__ span "Inconsistent state" (** 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 : config) (span : Meta.span) (generics : generic_args) (args : operand list) (dest : place) : cm_fun = fun ctx -> match (generics.regions, generics.types, generics.const_generics, args) with | [], [ boxed_ty ], [], [ Move input_box_place ] -> (* Required type checking *) let input_box = InterpreterPaths.read_place span Write input_box_place ctx in (let input_ty = ty_get_box input_box.ty in sanity_check __FILE__ __LINE__ (input_ty = boxed_ty)) span; (* Drop the value *) let ctx, cc = drop_value config span input_box_place ctx in (* Update the destination by setting it to [()] *) comp cc (assign_to_place config span mk_unit_value dest ctx) | _ -> craise __FILE__ __LINE__ span "Inconsistent state" (** Evaluate a non-local function call in concrete mode *) let eval_assumed_function_call_concrete (config : config) (span : Meta.span) (fid : assumed_fun_id) (call : call) : cm_fun = fun ctx -> let args = call.args in let dest = call.dest in match call.func with | FnOpMove _ -> (* Closure case: TODO *) craise __FILE__ __LINE__ span "Closures are not supported yet" | FnOpRegular func -> ( let generics = func.generics in (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) sanity_check __FILE__ __LINE__ (generics.const_generics = []) span; (* 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 | BoxFree -> (* Degenerate case: box_free *) eval_box_free config span generics args dest ctx | _ -> (* "Normal" case: not box_free *) (* Evaluate the operands *) (* let ctx, args_vl = eval_operands config ctx args in *) let args_vl, ctx, cc = eval_operands config span args ctx 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. *) (* Push the stack frame: we initialize the frame with the return variable, and one variable per input argument *) let ctx = push_frame ctx in (* Create and push the return variable *) let ret_vid = VarId.zero in let ret_ty = get_assumed_function_return_type span ctx fid generics in let ret_var = mk_var ret_vid (Some "@return") ret_ty in let ctx = push_uninitialized_var span ret_var ctx in (* Create and push the input variables *) let input_vars = VarId.mapi_from1 (fun id (v : typed_value) -> (mk_var id None v.ty, v)) args_vl in let ctx = push_vars span input_vars ctx 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 ctx, cf_eval_body = match fid with | BoxNew -> eval_box_new_concrete config span generics ctx | BoxFree -> (* Should have been treated above *) craise __FILE__ __LINE__ span "Unreachable" | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut -> craise __FILE__ __LINE__ span "Unimplemented" in let cc = cc_comp cc cf_eval_body in (* Pop the frame *) comp cc (pop_frame_assign config span dest ctx)) (** 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 : RegionGroupId.id -> abs_kind) (rgl : abs_region_group list) (region_can_end : RegionGroupId.id -> bool) : 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 : RegionId.Set.t AbstractionId.Map.t ref = ref AbstractionId.Map.empty in (* Auxiliary function to create one abstraction *) let create_abs (rg_id : RegionGroupId.id) (rg : abs_region_group) : abs = let abs_id = rg.id in let original_parents = rg.parents in let parents = List.fold_left (fun s pid -> AbstractionId.Set.add pid s) AbstractionId.Set.empty rg.parents in let regions = List.fold_left (fun s rid -> RegionId.Set.add rid s) RegionId.Set.empty rg.regions in let ancestors_regions = List.fold_left (fun acc parent_id -> RegionId.Set.union acc (AbstractionId.Map.find parent_id !abs_to_ancestors_regions)) RegionId.Set.empty rg.parents in let ancestors_regions_union_current_regions = RegionId.Set.union ancestors_regions regions in let can_end = region_can_end rg_id in abs_to_ancestors_regions := AbstractionId.Map.add abs_id ancestors_regions_union_current_regions !abs_to_ancestors_regions; (* Create the abstraction *) { abs_id; kind = kind rg_id; can_end; parents; original_parents; regions; ancestors_regions; avalues = []; } in (* Apply *) RegionGroupId.mapi create_abs rgl let create_push_abstractions_from_abs_region_groups (kind : RegionGroupId.id -> abs_kind) (rgl : abs_region_group list) (region_can_end : RegionGroupId.id -> bool) (compute_abs_avalues : abs -> eval_ctx -> eval_ctx * typed_avalue list) (ctx : eval_ctx) : 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 : eval_ctx) (abs : abs) : 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 = EAbs abs :: ctx.env } in (* Return *) ctx in List.fold_left insert_abs ctx empty_absl (** Auxiliary helper for [eval_transparent_function_call_symbolic] Instantiate the signature and introduce fresh abstractions and region ids while doing so. We perform some manipulations when instantiating the signature. # Trait impl calls ================== In particular, we have a special treatment of trait method calls when the trait ref is a known impl. For instance: {[ trait HasValue { fn has_value(&self) -> bool; } impl HasValue for Option { fn has_value(&self) { match self { None => false, Some(_) => true, } } } fn option_has_value(x: &Option) -> bool { x.has_value() } ]} The generated code looks like this: {[ structure HasValue (Self : Type) = { has_value : Self -> result bool } let OptionHasValueImpl.has_value (Self : Type) (self : Self) : result bool = match self with | None => false | Some _ => true let OptionHasValueInstance (T : Type) : HasValue (Option T) = { has_value = OptionHasValueInstance.has_value } ]} In [option_has_value], we don't want to refer to the [has_value] method of the instance of [HasValue] for [Option]. We want to refer directly to the function which implements [has_value] for [Option]. That is, instead of generating this: {[ let option_has_value (T : Type) (x : Option T) : result bool = (OptionHasValueInstance T).has_value x ]} We want to generate this: {[ let option_has_value (T : Type) (x : Option T) : result bool = OptionHasValueImpl.has_value T x ]} # Provided trait methods ======================== Calls to provided trait methods also have a special treatment because for now we forbid overriding provided trait methods in the trait implementations, which means that whenever we call a provided trait method, we do not refer to a trait clause but directly to the method provided in the trait declaration. *) let eval_transparent_function_call_symbolic_inst (span : Meta.span) (call : call) (ctx : eval_ctx) : fun_id_or_trait_method_ref * generic_args * (generic_args * trait_instance_id) option * fun_decl * region_var_groups * inst_fun_sig = match call.func with | FnOpMove _ -> (* Closure case: TODO *) craise __FILE__ __LINE__ span "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular fid) -> let def = ctx_lookup_fun_decl ctx fid in log#ldebug (lazy ("fun call:\n- call: " ^ call_to_string ctx call ^ "\n- call.generics:\n" ^ generic_args_to_string ctx func.generics ^ "\n- def.signature:\n" ^ fun_sig_to_string ctx def.signature)); let tr_self = UnknownTrait __FUNCTION__ in let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular fid) ctx.fun_ctx.regions_hierarchies in let inst_sg = instantiate_fun_sig span ctx func.generics tr_self def.signature regions_hierarchy in (func.func, func.generics, None, def, regions_hierarchy, inst_sg) | FunId (FAssumed _) -> (* Unreachable: must be a transparent function *) craise __FILE__ __LINE__ span "Unreachable" | TraitMethod (trait_ref, method_name, _) -> ( log#ldebug (lazy ("trait method call:\n- call: " ^ call_to_string ctx call ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n" ^ generic_args_to_string ctx func.generics ^ "\n- trait_ref.trait_decl_ref: " ^ trait_decl_ref_to_string ctx trait_ref.trait_decl_ref)); (* Lookup the trait method signature - there are several possibilities depending on whethere we call a top-level trait method impl or the method from a local clause *) match trait_ref.trait_id with | TraitImpl impl_id -> ( (* Lookup the trait impl *) let trait_impl = ctx_lookup_trait_impl ctx impl_id in log#ldebug (lazy ("trait impl: " ^ trait_impl_to_string ctx trait_impl)); (* First look in the required methods *) let method_id = List.find_opt (fun (s, _) -> s = method_name) trait_impl.required_methods in match method_id with | Some (_, id) -> (* This is a required method *) let method_def = ctx_lookup_fun_decl ctx id in (* We have to concatenate the generics for the impl and the generics for the method *) let generics = merge_generic_args trait_ref.generics func.generics in (* Instantiate *) let tr_self = TraitRef trait_ref in let fid : fun_id = FRegular id in let regions_hierarchy = LlbcAstUtils.FunIdMap.find fid ctx.fun_ctx.regions_hierarchies in let inst_sg = instantiate_fun_sig span ctx generics tr_self method_def.signature regions_hierarchy in (* Also update the function identifier: we want to forget the fact that we called a trait method, and treat it as a regular function call to the top-level function which implements the method. In order to do this properly, we also need to update the generics. *) let func = FunId fid in ( func, generics, Some (generics, tr_self), method_def, regions_hierarchy, inst_sg ) | None -> (* If not found, lookup the methods provided by the trait *declaration* (remember: for now, we forbid overriding provided methods) *) cassert __FILE__ __LINE__ (trait_impl.provided_methods = []) span "Overriding provided methods is currently forbidden"; let trait_decl = ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id in let _, method_id = List.find (fun (s, _) -> s = method_name) trait_decl.provided_methods in let method_id = Option.get method_id in let method_def = ctx_lookup_fun_decl ctx method_id in (* For the instantiation we have to do something peculiar because the method was defined for the trait declaration. We have to group: - the parameters given to the trait decl reference - the parameters given to the method itself For instance: {[ trait Foo { fn f(...) { ... } } fn g(x : G) where Clause0: Foo { x.f::(...) // The arguments to f are: } ]} *) let all_generics = TypesUtils.merge_generic_args trait_ref.trait_decl_ref.decl_generics func.generics in log#ldebug (lazy ("provided method call:" ^ "\n- method name: " ^ method_name ^ "\n- all_generics:\n" ^ generic_args_to_string ctx all_generics ^ "\n- parent params info: " ^ Print.option_to_string show_params_info method_def.signature.parent_params_info)); let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular method_id) ctx.fun_ctx.regions_hierarchies in let tr_self = TraitRef trait_ref in let inst_sg = instantiate_fun_sig span ctx all_generics tr_self method_def.signature regions_hierarchy in ( func.func, func.generics, Some (all_generics, tr_self), method_def, regions_hierarchy, inst_sg )) | _ -> (* We are using a local clause - we lookup the trait decl *) let trait_decl = ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id in (* Lookup the method decl in the required *and* the provided methods *) let _, method_id = let provided = List.filter_map (fun (id, f) -> match f with None -> None | Some f -> Some (id, f)) trait_decl.provided_methods in List.find (fun (s, _) -> s = method_name) (List.append trait_decl.required_methods provided) in let method_def = ctx_lookup_fun_decl ctx method_id in log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def)); (* Instantiate *) (* When instantiating, we need to group the generics for the trait ref and the generics for the method *) let generics = TypesUtils.merge_generic_args trait_ref.trait_decl_ref.decl_generics func.generics in let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular method_id) ctx.fun_ctx.regions_hierarchies in let tr_self = TraitRef trait_ref in let inst_sg = instantiate_fun_sig span ctx generics tr_self method_def.signature regions_hierarchy in ( func.func, func.generics, Some (generics, tr_self), method_def, regions_hierarchy, inst_sg ))) (** Evaluate a statement *) let rec eval_statement (config : config) (st : statement) : stl_cm_fun = fun 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 ~span:(Some st.span) ctx ^ "\n\n")); (* Take a snapshot of the current context for the purpose of generating pretty names *) let cc = S.save_snapshot ctx in (* Expand the symbolic values if necessary - we need to do that before checking the invariants *) let ctx, cc = comp cc (greedy_expand_symbolic_values config st.span ctx) in (* Sanity check *) Invariants.check_invariants st.span ctx; (* Evaluate the statement *) comp cc (eval_statement_raw config st ctx) and eval_statement_raw (config : config) (st : statement) : stl_cm_fun = fun ctx -> log#ldebug (lazy ("\neval_statement_raw: statement:\n" ^ statement_to_string_with_tab ctx st ^ "\n\n")); match st.content with | Assign (p, rvalue) -> ( (* We handle global assignments separately *) match rvalue with | Global (gid, generics) -> (* Evaluate the global *) eval_global config st.span p gid generics ctx | _ -> (* Evaluate the rvalue *) let res, ctx, cc = eval_rvalue_not_global config st.span rvalue ctx in (* Assign *) log#ldebug (lazy ("about to assign to place: " ^ place_to_string ctx p ^ "\n- Context:\n" ^ eval_ctx_to_string ~span:(Some st.span) ctx)); let (ctx, res), cf_assign = match res with | Error EPanic -> ((ctx, Panic), fun e -> e) | Ok rv -> (* Update the synthesized AST - here we store additional span-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...) *) let cc = match rvalue with | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable" | Len _ -> craise __FILE__ __LINE__ st.span "Len is not handled yet" | Use _ | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> let rp = rvalue_get_place rvalue in let rp = match rp with | Some rp -> Some (S.mk_mplace st.span rp ctx) | None -> None in S.synthesize_assignment ctx (S.mk_mplace st.span p ctx) rv rp in let ctx, cc = comp cc (assign_to_place config st.span rv p ctx) in ((ctx, Unit), cc) in let cc = cc_comp cc cf_assign in (* Compose and apply *) ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc)) | FakeRead p -> let ctx, cc = eval_fake_read config st.span p ctx in ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.span cc) | SetDiscriminant (p, variant_id) -> let (ctx, res), cc = set_discriminant config st.span p variant_id ctx in ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc) | Drop p -> let ctx, cc = drop_value config st.span p ctx in ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.span cc) | Assert assertion -> let (ctx, res), cc = eval_assertion config st.span assertion ctx in ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc) | Call call -> eval_function_call config st.span call ctx | Panic -> ([ (ctx, Panic) ], cf_singleton __FILE__ __LINE__ st.span) | Return -> ([ (ctx, Return) ], cf_singleton __FILE__ __LINE__ st.span) | Break i -> ([ (ctx, Break i) ], cf_singleton __FILE__ __LINE__ st.span) | Continue i -> ([ (ctx, Continue i) ], cf_singleton __FILE__ __LINE__ st.span) | Nop -> ([ (ctx, Unit) ], cf_singleton __FILE__ __LINE__ st.span) | Sequence (st1, st2) -> (* Evaluate the first statement *) let ctx_resl, cf_st1 = eval_statement config st1 ctx in (* Evaluate the sequence (evaluate the second statement if the first statement successfully evaluated, otherwise transfmit the control-flow break) *) let ctx_res_cfl = List.map (fun (ctx, res) -> match res with (* Evaluation successful: evaluate the second statement *) | Unit -> eval_statement config st2 ctx (* Control-flow break: transmit. We enumerate the cases on purpose *) | Panic | Break _ | Continue _ | Return | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> ([ (ctx, res) ], cf_singleton __FILE__ __LINE__ st.span)) ctx_resl in (* Put everything together: - we return the flattened list of contexts and results - we need to build the continuation which will build the whole expression from the continuations for the individual branches *) let ctx_resl, cf_st2 = comp_seqs __FILE__ __LINE__ st.span ctx_res_cfl in (ctx_resl, cc_comp cf_st1 cf_st2) | Loop loop_body -> let eval_loop_body = eval_statement config loop_body in InterpreterLoops.eval_loop config st.span eval_loop_body ctx | Switch switch -> eval_switch config st.span switch ctx | Error s -> craise __FILE__ __LINE__ st.span s and eval_global (config : config) (span : Meta.span) (dest : place) (gid : GlobalDeclId.id) (generics : generic_args) : stl_cm_fun = fun ctx -> let global = 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 *) let func = { func = FunId (FRegular global.body); generics } in let call = { func = FnOpRegular func; args = []; dest } in eval_transparent_function_call_concrete config span global.body call 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}). *) cassert __FILE__ __LINE__ (ty_no_regions global.ty) span "Const globals should not contain regions"; (* Instantiate the type *) (* There shouldn't be any reference to Self *) let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in let generics = Subst.generic_args_erase_regions generics in let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = Subst.make_subst_from_generics global.generics generics tr_self in let ty = Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self global.ty in let sval = mk_fresh_symbolic_value span ty in let ctx, cc = assign_to_place config span (mk_typed_value_from_symbolic_value sval) dest ctx in ( [ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ span (cc_comp (S.synthesize_global_eval gid generics sval) cc) ) (** Evaluate a switch *) and eval_switch (config : config) (span : Meta.span) (switch : switch) : stl_cm_fun = fun 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 *) match switch with | If (op, st1, st2) -> (* Evaluate the operand *) let op_v, ctx, cf_eval_op = eval_operand config span op ctx in (* Switch on the value *) let ctx_resl, cf_if = match op_v.value with | VLiteral (VBool b) -> (* Branch *) if b then eval_statement config st1 ctx else eval_statement config st2 ctx | VSymbolic sv -> (* Expand the symbolic boolean, and continue by evaluating the branches *) let (ctx_true, ctx_false), cf_bool = expand_symbolic_bool config span sv (S.mk_opt_place_from_op span op ctx) ctx in let resl_true = eval_statement config st1 ctx_true in let resl_false = eval_statement config st2 ctx_false in let ctx_resl, cf_branches = comp_seqs __FILE__ __LINE__ span [ resl_true; resl_false ] in let cc el = match cf_branches el with | [ e_true; e_false ] -> cf_bool (e_true, e_false) | _ -> internal_error __FILE__ __LINE__ span in (ctx_resl, cc) | _ -> craise __FILE__ __LINE__ span "Inconsistent state" in (* Compose *) (ctx_resl, cc_comp cf_eval_op cf_if) | SwitchInt (op, int_ty, stgts, otherwise) -> (* Evaluate the operand *) let op_v, ctx, cf_eval_op = eval_operand config span op ctx in (* Switch on the value *) let ctx_resl, cf_switch = match op_v.value with | VLiteral (VScalar sv) -> ( (* Sanity check *) sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) span; (* Find the branch *) match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with | None -> eval_statement config otherwise ctx | Some (_, tgt) -> eval_statement config tgt ctx) | VSymbolic sv -> (* 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 values, branches = List.split (List.concat (List.map (fun (vl, st) -> List.map (fun v -> (v, st)) vl) stgts)) in (* Expand the symbolic value *) let (ctx_branches, ctx_otherwise), cf_int = expand_symbolic_int config span sv (S.mk_opt_place_from_op span op ctx) int_ty values ctx in (* Evaluate the branches: first the "regular" branches *) let resl_branches = List.map (fun (ctx, branch) -> eval_statement config branch ctx) (List.combine ctx_branches branches) in (* Then evaluate the "otherwise" branch *) let resl_otherwise = eval_statement config otherwise ctx_otherwise in (* Compose the continuations *) let resl, cf = comp_seqs __FILE__ __LINE__ span (resl_branches @ [ resl_otherwise ]) in let cc el = let el, e_otherwise = Collections.List.pop_last el in cf_int (el, e_otherwise) in (resl, cc_comp cc cf) | _ -> craise __FILE__ __LINE__ span "Inconsistent state" in (* Compose *) (ctx_resl, cc_comp cf_eval_op cf_switch) | Match (p, stgts, otherwise) -> (* Access the place *) let access = Read in let expand_prim_copy = false in let p_v, ctx, cf_read_p = access_rplace_reorganize_and_read config span expand_prim_copy access p ctx in (* Match on the value *) let ctx_resl, cf_match = (* 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 | VAdt 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 -> ( match otherwise with | None -> craise __FILE__ __LINE__ span "No otherwise branch" | Some otherwise -> eval_statement config otherwise ctx) | Some (_, tgt) -> eval_statement config tgt ctx) | VSymbolic sv -> (* Expand the symbolic value - may lead to branching *) let ctxl, cf_expand = expand_symbolic_adt config span sv (Some (S.mk_mplace span p ctx)) ctx in (* Re-evaluate the switch - the value is not symbolic anymore, which means we will go to the other branch *) let resl = List.map (fun ctx -> (eval_switch config span switch) ctx) ctxl in (* Compose the continuations *) let ctx_resl, cf = comp_seqs __FILE__ __LINE__ span resl in (ctx_resl, cc_comp cf_expand cf) | _ -> craise __FILE__ __LINE__ span "Inconsistent state" in (* Compose *) (ctx_resl, cc_comp cf_read_p cf_match) (** Evaluate a function call (auxiliary helper for [eval_statement]) *) and eval_function_call (config : config) (span : Meta.span) (call : call) : stl_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 config.mode with | ConcreteMode -> eval_function_call_concrete config span call | SymbolicMode -> eval_function_call_symbolic config span call and eval_function_call_concrete (config : config) (span : Meta.span) (call : call) : stl_cm_fun = fun ctx -> match call.func with | FnOpMove _ -> craise __FILE__ __LINE__ span "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular fid) -> eval_transparent_function_call_concrete config span fid call ctx | FunId (FAssumed fid) -> (* 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... *) let ctx, cc = eval_assumed_function_call_concrete config span fid call ctx in ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ span cc) | TraitMethod _ -> craise __FILE__ __LINE__ span "Unimplemented") and eval_function_call_symbolic (config : config) (span : Meta.span) (call : call) : stl_cm_fun = match call.func with | FnOpMove _ -> craise __FILE__ __LINE__ span "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular _) | TraitMethod _ -> eval_transparent_function_call_symbolic config span call | FunId (FAssumed fid) -> eval_assumed_function_call_symbolic config span fid call func) (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) and eval_transparent_function_call_concrete (config : config) (span : Meta.span) (fid : FunDeclId.id) (call : call) : stl_cm_fun = fun ctx -> let args = call.args in let dest = call.dest in match call.func with | FnOpMove _ -> craise __FILE__ __LINE__ span "Closures are not supported yet" | FnOpRegular func -> let generics = func.generics in (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) sanity_check __FILE__ __LINE__ (generics.const_generics = []) span; (* Retrieve the (correctly instantiated) body *) let def = 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 -> craise __FILE__ __LINE__ span ("Can't evaluate a call to an opaque function: " ^ name_to_string ctx def.item_meta.name) | Some body -> body in (* TODO: we need to normalize the types if we want to correctly support traits *) cassert __FILE__ __LINE__ (generics.trait_refs = []) body.span "Traits are not supported yet in concrete mode"; (* There shouldn't be any reference to Self *) let tr_self = UnknownTrait __FUNCTION__ in let subst = Subst.make_subst_from_generics def.signature.generics generics tr_self in let locals, body_st = Subst.fun_body_substitute_in_body subst body in (* Evaluate the input operands *) sanity_check __FILE__ __LINE__ (List.length args = body.arg_count) body.span; let vl, ctx, cc = eval_operands config body.span args ctx 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 ctx = push_frame ctx 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) | _ -> craise __FILE__ __LINE__ span "Unreachable" in let input_locals, locals = Collections.List.split_at locals body.arg_count in let ctx = push_var span ret_var (mk_bottom span ret_var.var_ty) ctx in (* 2. Push the input values *) let ctx = let inputs = List.combine input_locals vl in (* Note that this function checks that the variables and their values * have the same type (this is important) *) push_vars span inputs ctx in (* 3. Push the remaining local variables (initialized as {!Bottom}) *) let ctx = push_uninitialized_vars span locals ctx in (* Execute the function body *) let ctx_resl, cc = comp cc (eval_function_body config body_st ctx) in (* Pop the stack frame and move the return value to its destination *) let ctx_resl_cfl = List.map (fun (ctx, res) -> match res with | Panic -> ((ctx, Panic), fun e -> e) | Return -> (* Pop the stack frame, retrieve the return value, move it to its destination and continue *) let ctx, cf = pop_frame_assign config span dest ctx in ((ctx, Unit), cf) | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> craise __FILE__ __LINE__ span "Unreachable") ctx_resl in let ctx_resl, cfl = List.split ctx_resl_cfl in let cf_pop el = List.map2 (fun cf e -> cf e) cfl el in (* Continue *) (ctx_resl, cc_comp cc cf_pop) (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) and eval_transparent_function_call_symbolic (config : config) (span : Meta.span) (call : call) : stl_cm_fun = fun ctx -> let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg = eval_transparent_function_call_symbolic_inst span call ctx in (* Sanity check: same number of inputs *) sanity_check __FILE__ __LINE__ (List.length call.args = List.length def.signature.inputs) def.item_meta.span; (* Sanity check: no nested borrows, borrows in ADTs, etc. *) cassert __FILE__ __LINE__ (List.for_all (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty)) (inst_sg.output :: inst_sg.inputs)) span "Nested borrows are not supported yet"; cassert __FILE__ __LINE__ (List.for_all (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty)) (inst_sg.output :: inst_sg.inputs)) span "ADTs containing borrows are not supported yet"; (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config def.item_meta.span func def.signature regions_hierarchy inst_sg generics trait_method_generics call.args call.dest 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. The [self_trait_ref] trait ref refers to [Self]. We use it when calling a provided trait method, because those methods have a special treatment: we dot not group them with the required trait methods, and forbid (for now) overriding them. We treat them as regular method, which take an additional trait ref as input. *) and eval_function_call_symbolic_from_inst_sig (config : config) (span : Meta.span) (fid : fun_id_or_trait_method_ref) (sg : fun_sig) (regions_hierarchy : region_var_groups) (inst_sg : inst_fun_sig) (generics : generic_args) (trait_method_generics : (generic_args * trait_instance_id) option) (args : operand list) (dest : place) : stl_cm_fun = fun ctx -> log#ldebug (lazy ("eval_function_call_symbolic_from_inst_sig:\n- fid: " ^ fun_id_or_trait_method_ref_to_string ctx fid ^ "\n- inst_sg:\n" ^ inst_fun_sig_to_string ctx inst_sg ^ "\n- call.generics:\n" ^ generic_args_to_string ctx generics ^ "\n- args:\n" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "\n- dest:\n" ^ place_to_string ctx dest)); (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.output in let ret_spc = mk_fresh_symbolic_value span 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 span p ctx) args in let dest_place = Some (S.mk_mplace span dest ctx) in (* Evaluate the input operands *) let args, ctx, cc = eval_operands config span args ctx in (* Generate the abstractions and insert them in the context *) let abs_ids = List.map (fun rg -> rg.id) inst_sg.regions_hierarchy in let args_with_rtypes = List.combine args inst_sg.inputs in (* Check the type of the input arguments *) cassert __FILE__ __LINE__ (List.for_all (fun ((arg, rty) : typed_value * rty) -> arg.ty = Subst.erase_regions rty) args_with_rtypes) span "The input arguments don't have the proper type"; (* 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 *) sanity_check __FILE__ __LINE__ (List.for_all (fun arg -> not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) args) span; (* 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 : abs) (ctx : eval_ctx) : eval_ctx * 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 span 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 = fresh_fun_call_id () in let region_can_end _ = true in let ctx = create_push_abstractions_from_abs_region_groups (fun rg_id -> FunCall (call_id, rg_id)) inst_sg.regions_hierarchy region_can_end compute_abs_avalues ctx in (* Synthesize the symbolic AST *) let cc = cc_comp cc (S.synthesize_regular_function_call fid call_id ctx sg regions_hierarchy abs_ids generics trait_method_generics args args_places ret_spc dest_place) in (* Move the return value to its destination *) let ctx, cc = comp cc (assign_to_place config span ret_value dest ctx) 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 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 = ctx_lookup_abs ctx abs_id in (* Check if it has parents *) AbstractionId.Set.is_empty abs.parents (* Check if it contains non-ignored loans *) && Option.is_none (InterpreterBorrowsCore .get_first_non_ignored_aloan_in_abstraction span 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 = AbstractionId.Set.of_list no_loans_abs in let ctx, cc = InterpreterBorrows.end_abstractions config span no_loans_abs ctx in (* Recursive call *) comp cc (end_abs_with_no_loans ctx)) else (* No abstractions to end: continue *) (ctx, fun e -> e) 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 ctx, cc = comp cc (if Config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output then end_abs_with_no_loans ctx else (ctx, fun e -> e)) 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... *) ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ span cc) (** Evaluate a non-local function call in symbolic mode *) and eval_assumed_function_call_symbolic (config : config) (span : Meta.span) (fid : assumed_fun_id) (call : call) (func : fn_ptr) : stl_cm_fun = fun ctx -> let generics = func.generics in let args = call.args in let dest = call.dest in (* Sanity check: make sure the type parameters don't contain regions - * this is a current limitation of our synthesis *) sanity_check __FILE__ __LINE__ (List.for_all (fun ty -> not (ty_has_borrows ctx.type_ctx.type_infos ty)) generics.types) span; (* 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 | BoxFree -> (* Degenerate case: box_free - note that this is not really a function * call: no need to call a "synthesize_..." function *) let ctx, cc = eval_box_free config span generics args dest ctx in ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ span cc) | _ -> (* "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 sg, regions_hierarchy, inst_sig = match fid with | BoxFree -> (* Should have been treated above *) craise __FILE__ __LINE__ span "Unreachable" | _ -> let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FAssumed fid) ctx.fun_ctx.regions_hierarchies in (* There shouldn't be any reference to Self *) let tr_self = UnknownTrait __FUNCTION__ in let sg = Assumed.get_assumed_fun_sig fid in let inst_sg = instantiate_fun_sig span ctx generics tr_self sg regions_hierarchy in (sg, regions_hierarchy, inst_sg) in (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config span (FunId (FAssumed fid)) sg regions_hierarchy inst_sig generics None args dest ctx (** Evaluate a statement seen as a function body *) and eval_function_body (config : config) (body : statement) : stl_cm_fun = fun ctx -> log#ldebug (lazy "eval_function_body:"); let ctx_resl, cf_body = eval_statement config body ctx in let ctx_res_cfl = List.map (fun (ctx, res) -> (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we delegate the check to the caller. *) log#ldebug (lazy "eval_function_body: cf_finish"); (* Expand the symbolic values if necessary - we need to do that before checking the invariants *) let ctx, cf = greedy_expand_symbolic_values config body.span ctx in (* Sanity check *) Invariants.check_invariants body.span ctx; (* Continue *) ((ctx, res), cf)) ctx_resl in let ctx_resl, cfl = List.split ctx_res_cfl in let cf_end el = List.map2 (fun cf e -> cf e) cfl el in (* Compose and continue *) (ctx_resl, cc_comp cf_body cf_end)