open Utils open LlbcAstUtils open Pure open PureUtils open InterpreterUtils open FunsAnalysis open TypesAnalysis open Errors module T = Types module V = Values module C = Contexts module A = LlbcAst module S = SymbolicAst module PP = PrintPure (** The local logger *) let log = Logging.symbolic_to_pure_log type type_ctx = { llbc_type_decls : T.type_decl TypeDeclId.Map.t; type_decls : type_decl TypeDeclId.Map.t; (** We use this for type-checking (for sanity checks) when translating values and functions. This map is empty when we translate the types, then contains all the translated types when we translate the functions. *) type_infos : type_infos; recursive_decls : T.TypeDeclId.Set.t; } [@@deriving show] type fun_sig_named_outputs = { sg : fun_sig; (** A function signature *) output_names : string option list; (** In case the signature is for a backward function, we may provides names for the outputs. The reason is that the outputs of backward functions come from (in case there are no nested borrows) borrows present in the inputs of the original rust function. In this situation, we can use the names of those inputs to name the outputs. Those names are very useful to generate beautiful codes (we may need to introduce temporary variables in the bodies of the backward functions to store the returned values, in which case we use those names). *) } [@@deriving show] type fun_ctx = { llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t; fun_infos : fun_info A.FunDeclId.Map.t; regions_hierarchies : T.region_var_groups FunIdMap.t; } [@@deriving show] type global_ctx = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t } [@@deriving show] type trait_decls_ctx = A.trait_decl A.TraitDeclId.Map.t [@@deriving show] type trait_impls_ctx = A.trait_impl A.TraitImplId.Map.t [@@deriving show] (** Whenever we translate a function call or an ended abstraction, we store the related information (this is useful when translating ended children abstractions). *) type call_info = { forward : S.call; forward_inputs : texpression list; (** Remember the list of inputs given to the forward function. Those inputs include the fuel and the state, if pertinent. *) back_funs : texpression option RegionGroupId.Map.t option; (** If we do not split between the forward/backward functions: the variables we introduced for the backward functions. Example: {[ let x, back = Vec.index_mut n v in ^^^^ here ... ]} The expression might be [None] in case the backward function has to be filtered (because it does nothing - the backward functions for shared borrows for instance). *) } [@@deriving show] (** Contains information about a loop we entered. Note that a path in a translated function body can have at most one call to a loop, because the loop function takes care of the end of the execution (and always happen at the end of the function). To be more precise, if we translate a function body which contains a loop, one of the leaves will be a call to the loop translation. The same happens for loop bodies. For instance, if in Rust we have: {[ fn get(...) { let x = f(...); loop { ... } } ]} Then in the translation we have: {[ let get_fwd ... = let x = f_fwd ... in (* We end the function by calling the loop translation *) get_fwd_loop ... ]} The various input and output fields are for this unique loop call, if there is one. *) type loop_info = { loop_id : LoopId.id; input_vars : var list; input_svl : V.symbolic_value list; generics : generic_args; forward_inputs : texpression list option; (** The forward inputs are initialized at [None] *) forward_output_no_state_no_result : texpression option; (** The forward outputs are initialized at [None] *) back_outputs : ty list RegionGroupId.Map.t; (** The map from region group ids to the types of the values given back by the corresponding loop abstractions. This map is partial. *) back_funs : texpression option RegionGroupId.Map.t option; (** Same as {!call_info.back_funs}. Initialized with [None], gets updated to [Some] only if we merge the fwd/back functions. *) fwd_effect_info : fun_effect_info; back_effect_infos : fun_effect_info RegionGroupId.Map.t; } [@@deriving show] (** Body synthesis context *) type bs_ctx = { (* TODO: there are a lot of duplications with the various decls ctx *) meta : Meta.meta; (** The meta information about the current declaration *) decls_ctx : C.decls_ctx; type_ctx : type_ctx; fun_ctx : fun_ctx; global_ctx : global_ctx; trait_decls_ctx : trait_decls_ctx; trait_impls_ctx : trait_impls_ctx; fun_dsigs : decomposed_fun_sig FunDeclId.Map.t; fun_decl : A.fun_decl; bid : RegionGroupId.id option; (** TODO: rename The id of the group region we are currently translating. If we split the forward/backward functions, we set this id at the very beginning of the translation. If we don't split, we set it to `None`, then update it when we enter an expression which is specific to a backward function. *) sg : decomposed_fun_sig; (** Information about the function signature - useful in particular to translate [Panic] *) sv_to_var : var V.SymbolicValueId.Map.t; (** Whenever we encounter a new symbolic value (introduced because of a symbolic expansion or upon ending an abstraction, for instance) we introduce a new variable (with a let-binding). *) var_counter : VarId.generator ref; (** Using a ref to make sure all the variables identifiers are unique. TODO: this is not very clean, and the code was initially written without a reference (and it's shape hasn't changed). We should use DeBruijn indices. *) state_var : VarId.id; (** The current state variable, in case the function is stateful *) back_state_vars : VarId.id RegionGroupId.Map.t; (** The additional input state variable received by a stateful backward function, **in case we are splitting the forward/backward functions**. When generating stateful functions, we generate code of the following form: {[ (st1, y) <-- f_fwd x st0; // st0 is the state upon calling f_fwd ... // the state may be updated (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back ]} When translating a backward function, we need at some point to update [state_var] with [back_state_var], to account for the fact that the state may have been updated by the caller between the call to the forward function and the call to the backward function. We also need to make sure we use the same variable in all the branches (because this variable is quantified at the definition level). *) fuel0 : VarId.id; (** The original fuel taken as input by the function (if we use fuel) *) fuel : VarId.id; (** The fuel to use for the recursive calls (if we use fuel) *) forward_inputs : var list; (** The input parameters for the forward function corresponding to the translated Rust inputs (no fuel, no state). *) backward_inputs_no_state : var list RegionGroupId.Map.t; (** The additional input parameters for the backward functions coming from the borrows consumed upon ending the lifetime (as a consequence those don't include the backward state, if there is one). If we split the forward/backward functions: we initialize this map when initializing the bs_ctx, because those variables are quantified at the definition level. Otherwise, we initialize it upon diving into the expressions which are specific to the backward functions. *) backward_inputs_with_state : var list RegionGroupId.Map.t; (** All the additional input parameters for the backward functions. Same remarks as for {!backward_inputs_no_state}. *) backward_outputs : var list option; (** The variables that the backward functions will output, corresponding to the borrows they give back (don't include the backward state). The translation is done as follows: - when we detect the ended input abstraction which corresponds to the backward function of the LLBC function we are translating, and which consumed the values [consumed_i] (that we need to give back to the caller), we introduce: {[ let v_i = consumed_i in ... ]} where the [v_i] are fresh, and are stored in the [backward_output]. - Then, upon reaching the [Return] node, we introduce: {[ return (v_i) ]} The option is [None] before we detect the ended input abstraction, and [Some] afterwards. *) calls : call_info V.FunCallId.Map.t; (** The function calls we encountered so far *) abstractions : (V.abs * texpression list) V.AbstractionId.Map.t; (** The ended abstractions we encountered so far, with their additional input arguments. We store it here and not in {!call_info} because we need a map from abstraction id to abstraction (and not from call id + region group id to abstraction). *) loop_ids_map : LoopId.id V.LoopId.Map.t; (** Ids to use for the loops *) loops : loop_info LoopId.Map.t; (** The loops we encountered so far. We are using a map to be general - in practice we will fail if we encounter more than one loop on a single path. *) loop_id : LoopId.id option; (** [Some] if we reached a loop (we are synthesizing a function, and reached a loop, or are synthesizing the loop body itself) *) inside_loop : bool; (** In case {!loop_id} is [Some]: - if [true]: we are synthesizing a loop body - if [false]: we reached a loop and are synthesizing the end of the function (after the loop body) Note that when a function contains a loop, we group the function symbolic AST and the loop symbolic AST in a single function. *) } [@@deriving show] (* TODO: move *) let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env = let type_decls = ctx.type_ctx.llbc_type_decls in let fun_decls = ctx.fun_ctx.llbc_fun_decls in let global_decls = ctx.global_ctx.llbc_global_decls in let trait_decls = ctx.trait_decls_ctx in let trait_impls = ctx.trait_impls_ctx in let { regions; types; const_generics; trait_clauses } : T.generic_params = ctx.fun_decl.signature.generics in let preds = ctx.fun_decl.signature.preds in { type_decls; fun_decls; global_decls; trait_decls; trait_impls; regions = [ regions ]; types; const_generics; trait_clauses; preds; locals = []; } let bs_ctx_to_pure_fmt_env (ctx : bs_ctx) : PrintPure.fmt_env = let type_decls = ctx.type_ctx.llbc_type_decls in let fun_decls = ctx.fun_ctx.llbc_fun_decls in let global_decls = ctx.global_ctx.llbc_global_decls in let trait_decls = ctx.trait_decls_ctx in let trait_impls = ctx.trait_impls_ctx in let generics = ctx.sg.generics in { type_decls; fun_decls; global_decls; trait_decls; trait_impls; generics; locals = []; } let ctx_generic_args_to_string (ctx : bs_ctx) (args : T.generic_args) : string = let env = bs_ctx_to_fmt_env ctx in Print.Types.generic_args_to_string env args let name_to_string (ctx : bs_ctx) = Print.Types.name_to_string (bs_ctx_to_fmt_env ctx) let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string = let env = bs_ctx_to_fmt_env ctx in Print.Values.symbolic_value_to_string env sv let typed_value_to_string (ctx : bs_ctx) (v : V.typed_value) : string = let env = bs_ctx_to_fmt_env ctx in Print.Values.typed_value_to_string ~meta:(Some ctx.meta) env v let pure_ty_to_string (ctx : bs_ctx) (ty : ty) : string = let env = bs_ctx_to_pure_fmt_env ctx in PrintPure.ty_to_string env false ty let pure_var_to_string (ctx : bs_ctx) (v : var) : string = let env = bs_ctx_to_pure_fmt_env ctx in PrintPure.var_to_string env v let ty_to_string (ctx : bs_ctx) (ty : T.ty) : string = let env = bs_ctx_to_fmt_env ctx in Print.Types.ty_to_string env ty let type_decl_to_string (ctx : bs_ctx) (def : T.type_decl) : string = let env = bs_ctx_to_fmt_env ctx in Print.Types.type_decl_to_string env def let pure_type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string = let env = bs_ctx_to_pure_fmt_env ctx in PrintPure.type_decl_to_string env def let texpression_to_string (ctx : bs_ctx) (e : texpression) : string = let env = bs_ctx_to_pure_fmt_env ctx in PrintPure.texpression_to_string ~metadata:(Some ctx.meta) env false "" " " e let fun_id_to_string (ctx : bs_ctx) (id : A.fun_id) : string = let env = bs_ctx_to_fmt_env ctx in Print.Expressions.fun_id_to_string env id let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string = let env = bs_ctx_to_pure_fmt_env ctx in PrintPure.fun_sig_to_string env sg let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string = let env = bs_ctx_to_pure_fmt_env ctx in PrintPure.fun_decl_to_string env def let typed_pattern_to_string (ctx : bs_ctx) (p : Pure.typed_pattern) : string = let env = bs_ctx_to_pure_fmt_env ctx in PrintPure.typed_pattern_to_string ~meta:(Some ctx.meta) env p let ctx_get_effect_info_for_bid (ctx : bs_ctx) (bid : RegionGroupId.id option) : fun_effect_info = match bid with | None -> ctx.sg.fwd_info.effect_info | Some bid -> let back_sg = RegionGroupId.Map.find bid ctx.sg.back_sg in back_sg.effect_info let ctx_get_effect_info (ctx : bs_ctx) : fun_effect_info = ctx_get_effect_info_for_bid ctx ctx.bid (* TODO: move *) let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string = let env = bs_ctx_to_fmt_env ctx in let verbose = false in let indent = "" in let indent_incr = " " in Print.Values.abs_to_string ~meta:(Some ctx.meta) env verbose indent indent_incr abs let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) : T.type_decl = TypeDeclId.Map.find id ctx.type_ctx.llbc_type_decls let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) : A.fun_decl = A.FunDeclId.Map.find id ctx.fun_ctx.llbc_fun_decls (* Some generic translation functions (we need to translate different "flavours" of types: forward types, backward types, etc.) *) let rec translate_generic_args (meta : Meta.meta) (translate_ty : T.ty -> ty) (generics : T.generic_args) : generic_args = (* We ignore the regions: if they didn't cause trouble for the symbolic execution, then everything's fine *) let types = List.map translate_ty generics.types in let const_generics = generics.const_generics in let trait_refs = List.map (translate_trait_ref meta translate_ty) generics.trait_refs in { types; const_generics; trait_refs } and translate_trait_ref (meta : Meta.meta) (translate_ty : T.ty -> ty) (tr : T.trait_ref) : trait_ref = let trait_id = translate_trait_instance_id meta translate_ty tr.trait_id in let generics = translate_generic_args meta translate_ty tr.generics in let trait_decl_ref = translate_trait_decl_ref meta translate_ty tr.trait_decl_ref in { trait_id; generics; trait_decl_ref } and translate_trait_decl_ref (meta : Meta.meta) (translate_ty : T.ty -> ty) (tr : T.trait_decl_ref) : trait_decl_ref = let decl_generics = translate_generic_args meta translate_ty tr.decl_generics in { trait_decl_id = tr.trait_decl_id; decl_generics } and translate_trait_instance_id (meta : Meta.meta) (translate_ty : T.ty -> ty) (id : T.trait_instance_id) : trait_instance_id = let translate_trait_instance_id = translate_trait_instance_id meta translate_ty in match id with | T.Self -> Self | TraitImpl id -> TraitImpl id | BuiltinOrAuto _ -> (* We should have eliminated those in the prepasses *) craise __FILE__ __LINE__ meta "Unreachable" | Clause id -> Clause id | ParentClause (inst_id, decl_id, clause_id) -> let inst_id = translate_trait_instance_id inst_id in ParentClause (inst_id, decl_id, clause_id) | ItemClause (inst_id, decl_id, item_name, clause_id) -> let inst_id = translate_trait_instance_id inst_id in ItemClause (inst_id, decl_id, item_name, clause_id) | TraitRef tr -> TraitRef (translate_trait_ref meta translate_ty tr) | FnPointer _ | Closure _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" | UnknownTrait s -> craise __FILE__ __LINE__ meta ("Unknown trait found: " ^ s) (** Translate a signature type - TODO: factor out the different translation functions *) let rec translate_sty (meta : Meta.meta) (ty : T.ty) : ty = let translate = translate_sty in match ty with | T.TAdt (type_id, generics) -> ( let generics = translate_sgeneric_args meta generics in match type_id with | T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics) | T.TTuple -> sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; mk_simpl_tuple_ty generics.types | T.TAssumed aty -> ( match aty with | T.TBox -> ( (* Eliminate the boxes *) match generics.types with | [ ty ] -> ty | _ -> craise __FILE__ __LINE__ meta "Box/vec/option type with incorrect number of arguments") | T.TArray -> TAdt (TAssumed TArray, generics) | T.TSlice -> TAdt (TAssumed TSlice, generics) | T.TStr -> TAdt (TAssumed TStr, generics))) | TVar vid -> TVar vid | TLiteral ty -> TLiteral ty | TNever -> craise __FILE__ __LINE__ meta "Unreachable" | TRef (_, rty, _) -> translate meta rty | TRawPtr (ty, rkind) -> let mut = match rkind with RMut -> Mut | RShared -> Const in let ty = translate meta ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) | TTraitType (trait_ref, type_name) -> let trait_ref = translate_strait_ref meta trait_ref in TTraitType (trait_ref, type_name) | TArrow _ -> craise __FILE__ __LINE__ meta "Arrow types are not supported yet" and translate_sgeneric_args (meta : Meta.meta) (generics : T.generic_args) : generic_args = translate_generic_args meta (translate_sty meta) generics and translate_strait_ref (meta : Meta.meta) (tr : T.trait_ref) : trait_ref = translate_trait_ref meta (translate_sty meta) tr and translate_strait_instance_id (meta : Meta.meta) (id : T.trait_instance_id) : trait_instance_id = translate_trait_instance_id meta (translate_sty meta) id let translate_trait_clause (meta : Meta.meta) (clause : T.trait_clause) : trait_clause = let { T.clause_id; meta = _; trait_id; clause_generics } = clause in let generics = translate_sgeneric_args meta clause_generics in { clause_id; trait_id; generics } let translate_strait_type_constraint (meta : Meta.meta) (ttc : T.trait_type_constraint) : trait_type_constraint = let { T.trait_ref; type_name; ty } = ttc in let trait_ref = translate_strait_ref meta trait_ref in let ty = translate_sty meta ty in { trait_ref; type_name; ty } let translate_predicates (meta : Meta.meta) (preds : T.predicates) : predicates = let trait_type_constraints = List.map (translate_strait_type_constraint meta) preds.trait_type_constraints in { trait_type_constraints } let translate_generic_params (meta : Meta.meta) (generics : T.generic_params) : generic_params = let { T.regions = _; types; const_generics; trait_clauses } = generics in let trait_clauses = List.map (translate_trait_clause meta) trait_clauses in { types; const_generics; trait_clauses } let translate_field (meta : Meta.meta) (f : T.field) : field = let field_name = f.field_name in let field_ty = translate_sty meta f.field_ty in { field_name; field_ty } let translate_fields (meta : Meta.meta) (fl : T.field list) : field list = List.map (translate_field meta) fl let translate_variant (meta : Meta.meta) (v : T.variant) : variant = let variant_name = v.variant_name in let fields = translate_fields meta v.fields in { variant_name; fields } let translate_variants (meta : Meta.meta) (vl : T.variant list) : variant list = List.map (translate_variant meta) vl (** Translate a type def kind from LLBC *) let translate_type_decl_kind (meta : Meta.meta) (kind : T.type_decl_kind) : type_decl_kind = match kind with | T.Struct fields -> Struct (translate_fields meta fields) | T.Enum variants -> Enum (translate_variants meta variants) | T.Opaque -> Opaque (** Translate a type definition from LLBC Remark: this is not symbolic to pure but LLBC to pure. Still, I don't see the point of moving this definition for now. *) let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : type_decl = log#ldebug (lazy (let ctx = Print.Contexts.decls_ctx_to_fmt_env ctx in "translate_type_decl:\n\n" ^ Print.Types.type_decl_to_string ctx def ^ "\n")); let env = Print.Contexts.decls_ctx_to_fmt_env ctx in let def_id = def.T.def_id in let llbc_name = def.name in let name = Print.Types.name_to_string env def.name in let { T.regions; types; const_generics; trait_clauses } = def.generics in (* Can't translate types with regions for now *) cassert __FILE__ __LINE__ (regions = []) def.meta "ADTs containing borrows are not supported yet"; let trait_clauses = List.map (translate_trait_clause def.meta) trait_clauses in let generics = { types; const_generics; trait_clauses } in let kind = translate_type_decl_kind def.meta def.T.kind in let preds = translate_predicates def.meta def.preds in let is_local = def.is_local in let meta = def.meta in { def_id; is_local; llbc_name; name; meta; generics; llbc_generics = def.generics; kind; preds; } let translate_type_id (meta : Meta.meta) (id : T.type_id) : type_id = match id with | TAdtId adt_id -> TAdtId adt_id | TAssumed aty -> let aty = match aty with | T.TArray -> TArray | T.TSlice -> TSlice | T.TStr -> TStr | T.TBox -> (* Boxes have to be eliminated: this type id shouldn't be translated *) craise __FILE__ __LINE__ meta "Unreachable" in TAssumed aty | TTuple -> TTuple (** Translate a type, seen as an input/output of a forward function (preserve all borrows, etc.). Remark: it doesn't matter whether the types has regions or erased regions (both cases happen, actually). TODO: factor out the various translation functions. *) let rec translate_fwd_ty (meta : Meta.meta) (type_infos : type_infos) (ty : T.ty) : ty = let translate = translate_fwd_ty meta type_infos in match ty with | T.TAdt (type_id, generics) -> ( let t_generics = translate_fwd_generic_args meta type_infos generics in (* Eliminate boxes and simplify tuples *) match type_id with | TAdtId _ | TAssumed (TArray | TSlice | TStr) -> let type_id = translate_type_id meta type_id in TAdt (type_id, t_generics) | TTuple -> (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the identity *) mk_simpl_tuple_ty t_generics.types | TAssumed TBox -> ( (* We eliminate boxes *) (* No general parametricity for now *) cassert __FILE__ __LINE__ (not (List.exists (TypesUtils.ty_has_borrows type_infos) generics.types)) meta "ADTs containing borrows are not supported yet"; match t_generics.types with | [ bty ] -> bty | _ -> craise __FILE__ __LINE__ meta "Unreachable: box/vec/option receives exactly one type \ parameter")) | TVar vid -> TVar vid | TNever -> craise __FILE__ __LINE__ meta "Unreachable" | TLiteral lty -> TLiteral lty | TRef (_, rty, _) -> translate rty | TRawPtr (ty, rkind) -> let mut = match rkind with RMut -> Mut | RShared -> Const in let ty = translate ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) | TTraitType (trait_ref, type_name) -> let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in TTraitType (trait_ref, type_name) | TArrow _ -> craise __FILE__ __LINE__ meta "Arrow types are not supported yet" and translate_fwd_generic_args (meta : Meta.meta) (type_infos : type_infos) (generics : T.generic_args) : generic_args = translate_generic_args meta (translate_fwd_ty meta type_infos) generics and translate_fwd_trait_ref (meta : Meta.meta) (type_infos : type_infos) (tr : T.trait_ref) : trait_ref = translate_trait_ref meta (translate_fwd_ty meta type_infos) tr and translate_fwd_trait_instance_id (meta : Meta.meta) (type_infos : type_infos) (id : T.trait_instance_id) : trait_instance_id = translate_trait_instance_id meta (translate_fwd_ty meta type_infos) id (** Simply calls [translate_fwd_ty] *) let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : T.ty) : ty = let type_infos = ctx.type_ctx.type_infos in translate_fwd_ty ctx.meta type_infos ty (** Simply calls [translate_fwd_generic_args] *) let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) : generic_args = let type_infos = ctx.type_ctx.type_infos in translate_fwd_generic_args ctx.meta type_infos generics (** Translate a type, when some regions may have ended. We return an option, because the translated type may be empty. [inside_mut]: are we inside a mutable borrow? *) let rec translate_back_ty (meta : Meta.meta) (type_infos : type_infos) (keep_region : T.region -> bool) (inside_mut : bool) (ty : T.ty) : ty option = let translate = translate_back_ty meta type_infos keep_region inside_mut in (* A small helper for "leave" types *) let wrap ty = if inside_mut then Some ty else None in match ty with | T.TAdt (type_id, generics) -> ( match type_id with | TAdtId _ | TAssumed (TArray | TSlice | TStr) -> let type_id = translate_type_id meta type_id in if inside_mut then (* We do not want to filter anything, so we translate the generics as "forward" types *) let generics = translate_fwd_generic_args meta type_infos generics in Some (TAdt (type_id, generics)) else (* If not inside a mutable reference: check if at least one of the generics contains a mutable reference (i.e., is not translated to `None`. If yes, keep the whole type, and translate all the generics as "forward" types (the backward function will extract the proper information from the ADT value) *) let types = List.filter_map translate generics.types in if types <> [] then let generics = translate_fwd_generic_args meta type_infos generics in Some (TAdt (type_id, generics)) else None | TAssumed TBox -> ( (* Don't accept ADTs (which are not tuples) with borrows for now *) cassert __FILE__ __LINE__ (not (TypesUtils.ty_has_borrows type_infos ty)) meta "ADTs containing borrows are not supported yet"; (* Eliminate the box *) match generics.types with | [ bty ] -> translate bty | _ -> craise __FILE__ __LINE__ meta "Unreachable: boxes receive exactly one type parameter") | TTuple -> ( (* Tuples can contain borrows (which we eliminate) *) let tys_t = List.filter_map translate generics.types in match tys_t with | [] -> None | _ -> (* Note that if there is exactly one type, [mk_simpl_tuple_ty] * is the identity *) Some (mk_simpl_tuple_ty tys_t))) | TVar vid -> wrap (TVar vid) | TNever -> craise __FILE__ __LINE__ meta "Unreachable" | TLiteral lty -> wrap (TLiteral lty) | TRef (r, rty, rkind) -> ( match rkind with | RShared -> (* Ignore shared references, unless we are below a mutable borrow *) if inside_mut then translate rty else None | RMut -> (* Dive in, remembering the fact that we are inside a mutable borrow *) let inside_mut = true in if keep_region r then translate_back_ty meta type_infos keep_region inside_mut rty else None) | TRawPtr _ -> (* TODO: not sure what to do here *) None | TTraitType (trait_ref, type_name) -> assert ( AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id); if inside_mut then (* Translate the trait ref as a "forward" trait ref - we do not want to filter any type *) let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in Some (TTraitType (trait_ref, type_name)) else None | TArrow _ -> craise __FILE__ __LINE__ meta "Arrow types are not supported yet" (** Simply calls [translate_back_ty] *) let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) (inside_mut : bool) (ty : T.ty) : ty option = let type_infos = ctx.type_ctx.type_infos in translate_back_ty ctx.meta type_infos keep_region inside_mut ty let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx = let const_generics = T.ConstGenericVarId.Map.of_list (List.map (fun (cg : T.const_generic_var) -> (cg.index, ctx_translate_fwd_ty ctx (T.TLiteral cg.ty))) ctx.sg.generics.const_generics) in let env = VarId.Map.empty in { PureTypeCheck.type_decls = ctx.type_ctx.type_decls; global_decls = ctx.global_ctx.llbc_global_decls; env; const_generics; } let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit = let meta = ctx.meta in let ctx = mk_type_check_ctx ctx in let _ = PureTypeCheck.check_typed_pattern meta ctx v in () let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit = if !Config.type_check_pure_code then let meta = ctx.meta in let ctx = mk_type_check_ctx ctx in PureTypeCheck.check_texpression meta ctx e let translate_fun_id_or_trait_method_ref (ctx : bs_ctx) (id : A.fun_id_or_trait_method_ref) : fun_id_or_trait_method_ref = match id with | FunId fun_id -> FunId fun_id | TraitMethod (trait_ref, method_name, fun_decl_id) -> let type_infos = ctx.type_ctx.type_infos in let trait_ref = translate_fwd_trait_ref ctx.meta type_infos trait_ref in TraitMethod (trait_ref, method_name, fun_decl_id) let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call) (args : texpression list) (back_funs : texpression option RegionGroupId.Map.t option) (ctx : bs_ctx) : bs_ctx = let calls = ctx.calls in sanity_check __FILE__ __LINE__ (not (V.FunCallId.Map.mem call_id calls)) ctx.meta; let info = { forward; forward_inputs = args; back_funs } in let calls = V.FunCallId.Map.add call_id info calls in { ctx with calls } (** [inherit_args]: the list of inputs inherited from the forward function and the ancestors backward functions, if pertinent. [back_args]: the *additional* list of inputs received by the backward function, including the state. Returns the updated context and the expression corresponding to the function that we need to call. This function may be [None] if it has to be ignored (because it does nothing). *) let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id) (back_id : T.RegionGroupId.id) (back_args : texpression list) (ctx : bs_ctx) : bs_ctx * texpression option = (* Insert the abstraction in the call informations *) let info = V.FunCallId.Map.find call_id ctx.calls in let calls = V.FunCallId.Map.add call_id info ctx.calls in (* Insert the abstraction in the abstractions map *) let abstractions = ctx.abstractions in sanity_check __FILE__ __LINE__ (not (V.AbstractionId.Map.mem abs.abs_id abstractions)) ctx.meta; let abstractions = V.AbstractionId.Map.add abs.abs_id (abs, back_args) abstractions in (* Compute the expression corresponding to the function. We simply lookup the variable introduced for the backward function. *) let func = RegionGroupId.Map.find back_id (Option.get info.back_funs) in (* Update the context and return *) ({ ctx with calls; abstractions }, func) (** List the ancestors of an abstraction *) let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) : V.AbstractionId.id list = (* We could do something more "elegant" without references, but it is * so much simpler to use references... *) let abs_set = ref V.AbstractionId.Set.empty in let rec gather (abs_id : V.AbstractionId.id) : unit = if V.AbstractionId.Set.mem abs_id !abs_set then () else ( abs_set := V.AbstractionId.Set.add abs_id !abs_set; let abs, _ = V.AbstractionId.Map.find abs_id ctx.abstractions in List.iter gather abs.original_parents) in List.iter gather abs.original_parents; let ids = !abs_set in (* List the ancestors, in the proper order *) let call_info = V.FunCallId.Map.find call_id ctx.calls in List.filter (fun id -> V.AbstractionId.Set.mem id ids) call_info.forward.abstractions (** List the ancestor abstractions of an abstraction introduced because of a function call *) let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) : (V.abs * texpression list) list = let abs_ids = list_ancestor_abstractions_ids ctx abs call_id in List.map (fun id -> V.AbstractionId.Map.find id ctx.abstractions) abs_ids (** Small utility. Does the function *decrease* the fuel? [true] if recursive. *) let function_decreases_fuel (info : fun_effect_info) : bool = !Config.use_fuel && info.is_rec (** Small utility. Does the function *use* the fuel? [true] if can diverge. *) let function_uses_fuel (info : fun_effect_info) : bool = !Config.use_fuel && info.can_diverge (** Small utility *) let mk_fuel_input_ty_as_list (info : fun_effect_info) : ty list = if function_uses_fuel info then [ mk_fuel_ty ] else [] (** Small utility *) let mk_fuel_input_as_list (ctx : bs_ctx) (info : fun_effect_info) : texpression list = if function_uses_fuel info then [ mk_fuel_texpression ctx.fuel ] else [] (** Small utility. *) let compute_raw_fun_effect_info (meta : Meta.meta) (fun_infos : fun_info A.FunDeclId.Map.t) (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option) (gid : T.RegionGroupId.id option) : fun_effect_info = match fun_id with | TraitMethod (_, _, fid) | FunId (FRegular fid) -> let info = A.FunDeclId.Map.find fid fun_infos in let stateful_group = info.stateful in let stateful = stateful_group && ((not !Config.backward_no_state_update) || gid = None) in { can_fail = info.can_fail; stateful_group; stateful; can_diverge = info.can_diverge; is_rec = info.is_rec || Option.is_some lid; } | FunId (FAssumed aid) -> sanity_check __FILE__ __LINE__ (lid = None) meta; { can_fail = Assumed.assumed_fun_can_fail aid; stateful_group = false; stateful = false; can_diverge = false; is_rec = false; } (** TODO: not very clean. *) let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option) (gid : T.RegionGroupId.id option) : fun_effect_info = match lid with | None -> ( match fun_id with | TraitMethod (_, _, fid) | FunId (FRegular fid) -> let dsg = A.FunDeclId.Map.find fid ctx.fun_dsigs in let info = match gid with | None -> dsg.fwd_info.effect_info | Some gid -> (RegionGroupId.Map.find gid dsg.back_sg).effect_info in { info with is_rec = info.is_rec || Option.is_some lid } | FunId (FAssumed _) -> compute_raw_fun_effect_info ctx.meta ctx.fun_ctx.fun_infos fun_id lid gid) | Some lid -> ( (* This is necessarily for the current function *) match fun_id with | FunId (FRegular fid) -> ( sanity_check __FILE__ __LINE__ (fid = ctx.fun_decl.def_id) ctx.meta; (* Lookup the loop *) let lid = V.LoopId.Map.find lid ctx.loop_ids_map in let loop_info = LoopId.Map.find lid ctx.loops in match gid with | None -> loop_info.fwd_effect_info | Some gid -> RegionGroupId.Map.find gid loop_info.back_effect_infos) | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable") (** Translate a function signature to a decomposed function signature. Note that the function also takes a list of names for the inputs, and computes, for every output for the backward functions, a corresponding name (outputs for backward functions come from borrows in the inputs of the forward function) which we use as hints to generate pretty names in the extracted code. We use [bid] ("backward function id") only if we split the forward and the backward functions. *) let translate_fun_sig_with_regions_hierarchy_to_decomposed (meta : Meta.meta) (decls_ctx : C.decls_ctx) (fun_id : A.fun_id_or_trait_method_ref) (regions_hierarchy : T.region_var_groups) (sg : A.fun_sig) (input_names : string option list) : decomposed_fun_sig = let fun_infos = decls_ctx.fun_ctx.fun_infos in let type_infos = decls_ctx.type_ctx.type_infos in (* We need an evaluation context to normalize the types (to normalize the associated types, etc. - for instance it may happen that the types refer to the types associated to a trait ref, but where the trait ref is a known impl). *) (* Create the context *) let ctx = let region_groups = List.map (fun (g : T.region_var_group) -> g.id) regions_hierarchy in let ctx = InterpreterUtils.initialize_eval_ctx meta decls_ctx region_groups sg.generics.types sg.generics.const_generics in (* Compute the normalization map for the *sty* types and add it to the context *) AssociatedTypes.ctx_add_norm_trait_types_from_preds meta ctx sg.preds.trait_type_constraints in (* Normalize the signature *) let sg = let ({ A.inputs; output; _ } : A.fun_sig) = sg in let norm = AssociatedTypes.ctx_normalize_ty meta ctx in let inputs = List.map norm inputs in let output = norm output in { sg with A.inputs; output } in (* Is the forward function stateful, and can it fail? *) let fwd_effect_info = compute_raw_fun_effect_info meta fun_infos fun_id None None in (* Compute the forward inputs *) let fwd_fuel = mk_fuel_input_ty_as_list fwd_effect_info in let fwd_inputs_no_fuel_no_state = List.map (translate_fwd_ty meta type_infos) sg.inputs in (* State input for the forward function *) let fwd_state_ty = (* For the forward state, we check if the *whole group* is stateful. See {!effect_info}. *) if fwd_effect_info.stateful_group then [ mk_state_ty ] else [] in let fwd_inputs = List.concat [ fwd_fuel; fwd_inputs_no_fuel_no_state; fwd_state_ty ] in (* Compute the backward output, without the effect information *) let fwd_output = translate_fwd_ty meta type_infos sg.output in (* Compute the type information for the backward function *) (* Small helper to translate types for backward functions *) let translate_back_ty_for_gid (gid : T.RegionGroupId.id) (ty : T.ty) : ty option = let rg = T.RegionGroupId.nth regions_hierarchy gid in (* Turn *all* the outer bound regions into free regions *) let _, rid_subst, r_subst = Substitute.fresh_regions_with_substs_from_vars ~fail_if_not_found:true sg.generics.regions in let subst = { Substitute.empty_subst with r_subst } in let ty = Substitute.ty_substitute subst ty in (* Compute the set of regions belonging to this group *) let gr_regions = T.RegionId.Set.of_list (List.map (fun rid -> Option.get (rid_subst rid)) rg.regions) in let keep_region r = match r with | T.RStatic -> raise Unimplemented | RErased -> craise __FILE__ __LINE__ meta "Unexpected erased region" | RBVar _ -> craise __FILE__ __LINE__ meta "Unexpected bound region" | RFVar rid -> T.RegionId.Set.mem rid gr_regions in let inside_mut = false in translate_back_ty meta type_infos keep_region inside_mut ty in let translate_back_inputs_for_gid (gid : T.RegionGroupId.id) : ty list = (* For now we don't supported nested borrows, so we check that there aren't parent regions *) let parents = list_ancestor_region_groups regions_hierarchy gid in cassert __FILE__ __LINE__ (T.RegionGroupId.Set.is_empty parents) meta "Nested borrows are not supported yet"; (* For now, we don't allow nested borrows, so the additional inputs to the backward function can only come from borrows that were returned like in (for the backward function we introduce for 'a): {[ fn f<'a>(...) -> &'a mut u32; ]} Upon ending the abstraction for 'a, we need to get back the borrow the function returned. *) let inputs = List.filter_map (translate_back_ty_for_gid gid) [ sg.output ] in log#ldebug (lazy (let ctx = Print.Contexts.decls_ctx_to_fmt_env decls_ctx in let pctx = PrintPure.decls_ctx_to_fmt_env decls_ctx in let output = Print.Types.ty_to_string ctx sg.output in let inputs = Print.list_to_string (PrintPure.ty_to_string pctx false) inputs in "translate_back_inputs_for_gid:" ^ "\n- gid: " ^ RegionGroupId.to_string gid ^ "\n- output: " ^ output ^ "\n- back inputs: " ^ inputs ^ "\n")); inputs in let compute_back_outputs_for_gid (gid : RegionGroupId.id) : string option list * ty list = (* The outputs are the borrows inside the regions of the abstractions and which are present in the input values. For instance, see: {[ fn f<'a>(x : &'a mut u32) -> ...; ]} Upon ending the abstraction for 'a, we give back the borrow which was consumed through the [x] parameter. *) let outputs = List.map (fun (name, input_ty) -> (name, translate_back_ty_for_gid gid input_ty)) (List.combine input_names sg.inputs) in (* Filter *) let outputs = List.filter (fun (_, opt_ty) -> Option.is_some opt_ty) outputs in let outputs = List.map (fun (name, opt_ty) -> (name, Option.get opt_ty)) outputs in let names, outputs = List.split outputs in log#ldebug (lazy (let ctx = Print.Contexts.decls_ctx_to_fmt_env decls_ctx in let pctx = PrintPure.decls_ctx_to_fmt_env decls_ctx in let inputs = Print.list_to_string (Print.Types.ty_to_string ctx) sg.inputs in let outputs = Print.list_to_string (PrintPure.ty_to_string pctx false) outputs in "compute_back_outputs_for_gid:" ^ "\n- gid: " ^ RegionGroupId.to_string gid ^ "\n- inputs: " ^ inputs ^ "\n- back outputs: " ^ outputs ^ "\n")); (names, outputs) in let compute_back_info_for_group (rg : T.region_var_group) : RegionGroupId.id * back_sg_info = let gid = rg.id in let back_effect_info = compute_raw_fun_effect_info meta fun_infos fun_id None (Some gid) in let inputs_no_state = translate_back_inputs_for_gid gid in let inputs_no_state = List.map (fun ty -> (Some "ret", ty)) inputs_no_state in (* We consider a backward function as stateful and potentially failing **only if it has inputs** (for the "potentially failing": if it has not inputs, we directly evaluate it in the body of the forward function). For instance, we do the following: {[ // Rust fn push(v : &mut Vec, x : T) { ... } (* Generated code: before doing unit elimination. We return (), as well as the backward function; as the backward function doesn't consume any inputs, it is a value that we compute directly in the body of [push]. *) let push T (v : Vec T) (x : T) : Result (() * Vec T) = ... (* Generated code: after doing unit elimination, if we simplify the merged fwd/back functions (see below). *) let push T (v : Vec T) (x : T) : Result (Vec T) = ... ]} *) let back_effect_info = let b = inputs_no_state <> [] in { back_effect_info with stateful = back_effect_info.stateful && b; can_fail = back_effect_info.can_fail && b; } in let state = if back_effect_info.stateful then [ (None, mk_state_ty) ] else [] in let inputs = inputs_no_state @ state in let output_names, outputs = compute_back_outputs_for_gid gid in let filter = !Config.simplify_merged_fwd_backs && inputs = [] && outputs = [] in let info = { inputs; inputs_no_state; outputs; output_names; effect_info = back_effect_info; filter; } in (gid, info) in let back_sg = RegionGroupId.Map.of_list (List.map compute_back_info_for_group regions_hierarchy) in (* The additional information about the forward function *) let fwd_info = (* *) let has_fuel = fwd_fuel <> [] in let num_inputs_no_fuel_no_state = List.length fwd_inputs_no_fuel_no_state in let num_inputs_with_fuel_no_state = (* We use the fact that [fuel] has length 1 if we use some fuel, 0 otherwise *) List.length fwd_fuel + num_inputs_no_fuel_no_state in let fwd_info : inputs_info = { has_fuel; num_inputs_no_fuel_no_state; num_inputs_with_fuel_no_state; num_inputs_with_fuel_with_state = (* We use the fact that [fwd_state_ty] has length 1 if there is a state, and 0 otherwise *) num_inputs_with_fuel_no_state + List.length fwd_state_ty; } in let ignore_output = if !Config.simplify_merged_fwd_backs then ty_is_unit fwd_output && List.exists (fun (info : back_sg_info) -> not info.filter) (RegionGroupId.Map.values back_sg) else false in let info = { fwd_info; effect_info = fwd_effect_info; ignore_output } in sanity_check __FILE__ __LINE__ (fun_sig_info_is_wf info) meta; info in (* Generic parameters *) let generics = translate_generic_params meta sg.generics in (* Return *) let preds = translate_predicates meta sg.preds in { generics; llbc_generics = sg.generics; preds; fwd_inputs; fwd_output; back_sg; fwd_info; } let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx) (fun_id : FunDeclId.id) (sg : A.fun_sig) (input_names : string option list) : decomposed_fun_sig = (* Retrieve the list of parent backward functions *) let regions_hierarchy = FunIdMap.find (FRegular fun_id) decls_ctx.fun_ctx.regions_hierarchies in let meta = (FunDeclId.Map.find fun_id decls_ctx.fun_ctx.fun_decls).meta in translate_fun_sig_with_regions_hierarchy_to_decomposed meta decls_ctx (FunId (FRegular fun_id)) regions_hierarchy sg input_names let translate_fun_sig_from_decl_to_decomposed (decls_ctx : C.decls_ctx) (fdef : LlbcAst.fun_decl) : decomposed_fun_sig = let input_names = match fdef.body with | None -> List.map (fun _ -> None) fdef.signature.inputs | Some body -> List.map (fun (v : LlbcAst.var) -> v.name) (LlbcAstUtils.fun_body_get_input_vars body) in let sg = translate_fun_sig_to_decomposed decls_ctx fdef.def_id fdef.signature input_names in log#ldebug (lazy ("translate_fun_sig_from_decl_to_decomposed:" ^ "\n- name: " ^ T.show_name fdef.name ^ "\n- sg:\n" ^ show_decomposed_fun_sig sg ^ "\n")); sg let mk_output_ty_from_effect_info (effect_info : fun_effect_info) (ty : ty) : ty = let output = if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; ty ] else ty in if effect_info.can_fail then mk_result_ty output else output let mk_back_output_ty_from_effect_info (effect_info : fun_effect_info) (inputs : ty list) (ty : ty) : ty = let output = if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; ty ] else ty in if effect_info.can_fail && inputs <> [] then mk_result_ty output else output (** Compute the arrow types for all the backward functions. If a backward function has no inputs/outputs we filter it. We may also filter the region group ids (param [keep_rg_ids]). This is useful for the loops: not all the parent function region groups can be linked to a region abstraction introduced by the loop. *) let compute_back_tys_with_info (dsg : Pure.decomposed_fun_sig) ?(keep_rg_ids : RegionGroupId.Set.t option = None) (subst : (generic_args * trait_instance_id) option) : (back_sg_info * ty) option list = let keep_rg_id = match keep_rg_ids with | None -> fun _ -> true | Some ids -> fun id -> RegionGroupId.Set.mem id ids in List.map (fun ((rg_id, back_sg) : RegionGroupId.id * back_sg_info) -> if keep_rg_id rg_id then let effect_info = back_sg.effect_info in (* Compute the input/output types *) let inputs = List.map snd back_sg.inputs in let outputs = back_sg.outputs in (* Filter if necessary *) if !Config.simplify_merged_fwd_backs && inputs = [] && outputs = [] then None else let output = mk_simpl_tuple_ty outputs in let output = mk_back_output_ty_from_effect_info effect_info inputs output in let ty = mk_arrows inputs output in (* Substitute - TODO: normalize *) let ty = match subst with | None -> ty | Some (generics, tr_self) -> let subst = make_subst_from_generics dsg.generics generics tr_self in ty_substitute subst ty in Some (back_sg, ty) else (* We ignore this region group *) None) (RegionGroupId.Map.bindings dsg.back_sg) let compute_back_tys (dsg : Pure.decomposed_fun_sig) ?(keep_rg_ids : RegionGroupId.Set.t option = None) (subst : (generic_args * trait_instance_id) option) : ty option list = List.map (Option.map snd) (compute_back_tys_with_info dsg ~keep_rg_ids subst) (** Compute the output type of a function, from a decomposed signature (the output type contains the type of the value returned by the forward function as well as the types of the returned backward functions). *) let compute_output_ty_from_decomposed (dsg : Pure.decomposed_fun_sig) : ty = (* Compute the arrow types for all the backward functions *) let back_tys = List.filter_map (fun x -> x) (compute_back_tys dsg None) in (* Group the forward output and the types of the backward functions *) let effect_info = dsg.fwd_info.effect_info in let output = (* We might need to ignore the output of the forward function (if it is unit for instance) *) let tys = if dsg.fwd_info.ignore_output then back_tys else dsg.fwd_output :: back_tys in mk_simpl_tuple_ty tys in mk_output_ty_from_effect_info effect_info output let translate_fun_sig_from_decomposed (dsg : Pure.decomposed_fun_sig) : fun_sig = let generics = dsg.generics in let llbc_generics = dsg.llbc_generics in let preds = dsg.preds in (* Compute the effects info *) let fwd_info = dsg.fwd_info in let back_effect_info = RegionGroupId.Map.of_list (List.map (fun ((gid, info) : RegionGroupId.id * back_sg_info) -> (gid, info.effect_info)) (RegionGroupId.Map.bindings dsg.back_sg)) in let inputs, output = let output = compute_output_ty_from_decomposed dsg in let inputs = dsg.fwd_inputs in (inputs, output) in { generics; llbc_generics; preds; inputs; output; fwd_info; back_effect_info } let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * var * typed_pattern = (* Generate the fresh variable *) let id, var_counter = VarId.fresh !(ctx.var_counter) in let state_var = { id; basename = Some ConstStrings.state_basename; ty = mk_state_ty } in let state_pat = mk_typed_pattern_from_var state_var None in (* Update the context *) ctx.var_counter := var_counter; let ctx = { ctx with state_var = id } in (* Return *) (ctx, state_var, state_pat) (** WARNING: do not call this function directly. Call [fresh_named_var_for_symbolic_value] instead. *) let fresh_var_llbc_ty (basename : string option) (ty : T.ty) (ctx : bs_ctx) : bs_ctx * var = (* Generate the fresh variable *) let id, var_counter = VarId.fresh !(ctx.var_counter) in let ty = ctx_translate_fwd_ty ctx ty in let var = { id; basename; ty } in (* Update the context *) ctx.var_counter := var_counter; (* Return *) (ctx, var) let fresh_named_var_for_symbolic_value (basename : string option) (sv : V.symbolic_value) (ctx : bs_ctx) : bs_ctx * var = (* Generate the fresh variable *) let ctx, var = fresh_var_llbc_ty basename sv.sv_ty ctx in (* Insert in the map *) let sv_to_var = V.SymbolicValueId.Map.add_strict sv.sv_id var ctx.sv_to_var in (* Update the context *) let ctx = { ctx with sv_to_var } in (* Return *) (ctx, var) let fresh_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : bs_ctx * var = fresh_named_var_for_symbolic_value None sv ctx let fresh_vars_for_symbolic_values (svl : V.symbolic_value list) (ctx : bs_ctx) : bs_ctx * var list = List.fold_left_map (fun ctx sv -> fresh_var_for_symbolic_value sv ctx) ctx svl let fresh_named_vars_for_symbolic_values (svl : (string option * V.symbolic_value) list) (ctx : bs_ctx) : bs_ctx * var list = List.fold_left_map (fun ctx (name, sv) -> fresh_named_var_for_symbolic_value name sv ctx) ctx svl (** This generates a fresh variable **which is not to be linked to any symbolic value** *) let fresh_var (basename : string option) (ty : ty) (ctx : bs_ctx) : bs_ctx * var = (* Generate the fresh variable *) let id, var_counter = VarId.fresh !(ctx.var_counter) in let var = { id; basename; ty } in (* Update the context *) ctx.var_counter := var_counter; (* Return *) (ctx, var) let fresh_vars (vars : (string option * ty) list) (ctx : bs_ctx) : bs_ctx * var list = List.fold_left_map (fun ctx (name, ty) -> fresh_var name ty ctx) ctx vars let fresh_opt_vars (vars : (string option * ty) option list) (ctx : bs_ctx) : bs_ctx * var option list = List.fold_left_map (fun ctx var -> match var with | None -> (ctx, None) | Some (name, ty) -> let ctx, var = fresh_var name ty ctx in (ctx, Some var)) ctx vars (* Introduce variables for the backward functions. We may filter the region group ids. This is useful for the loops: not all the parent function region groups can be linked to a region abstraction introduced by the loop. *) let fresh_back_vars_for_current_fun (ctx : bs_ctx) (keep_rg_ids : RegionGroupId.Set.t option) : bs_ctx * var option list = (* We lookup the LLBC definition in an attempt to derive pretty names for the backward functions. *) let back_var_names = let def_id = ctx.fun_decl.def_id in let sg = ctx.fun_decl.signature in let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular def_id) ctx.fun_ctx.regions_hierarchies in List.map (fun (gid, _) -> let rg = RegionGroupId.nth regions_hierarchy gid in let region_names = List.map (fun rid -> (T.RegionVarId.nth sg.generics.regions rid).name) rg.regions in let name = match region_names with | [] -> "back" | [ Some r ] -> "back" ^ r | _ -> (* Concatenate all the region names *) "back" ^ String.concat "" (List.filter_map (fun x -> x) region_names) in Some name) (RegionGroupId.Map.bindings ctx.sg.back_sg) in let back_vars = List.combine back_var_names (compute_back_tys ctx.sg ~keep_rg_ids None) in let back_vars = List.map (fun (name, ty) -> match ty with None -> None | Some ty -> Some (name, ty)) back_vars in fresh_opt_vars back_vars ctx (** IMPORTANT: do not use this one directly, but rather {!symbolic_value_to_texpression} *) let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = match V.SymbolicValueId.Map.find_opt sv.sv_id ctx.sv_to_var with | Some v -> v | None -> craise __FILE__ __LINE__ ctx.meta ("Could not find var for symbolic value: " ^ V.SymbolicValueId.to_string sv.sv_id) (** Peel boxes as long as the value is of the form [Box] *) let rec unbox_typed_value (meta : Meta.meta) (v : V.typed_value) : V.typed_value = match (v.value, v.ty) with | V.VAdt av, T.TAdt (T.TAssumed T.TBox, _) -> ( match av.field_values with | [ bv ] -> unbox_typed_value meta bv | _ -> craise __FILE__ __LINE__ meta "Unreachable") | _ -> v (** Translate a symbolic value. Because we do not necessarily introduce variables for the symbolic values of (translated) type unit, it is important that we do not lookup variables in case the symbolic value has type unit. *) let symbolic_value_to_texpression (ctx : bs_ctx) (sv : V.symbolic_value) : texpression = (* Translate the type *) let ty = ctx_translate_fwd_ty ctx sv.sv_ty in (* If the type is unit, directly return unit *) if ty_is_unit ty then mk_unit_rvalue else (* Otherwise lookup the variable *) let var = lookup_var_for_symbolic_value sv ctx in mk_texpression_from_var var (** Translate a typed value. It is used, for instance, on values used as inputs for function calls. **IMPORTANT**: this function makes the assumption that the typed value doesn't contain ⊥. This means in particular that symbolic values don't contain ended regions. TODO: we might want to remember in the symbolic AST the set of ended regions, at the points where we need it, for sanity checks (though the sanity checks in the symbolic interpreter should be enough). The points where we need this set so far: - function call - end abstraction - return *) let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) (v : V.typed_value) : texpression = (* We need to ignore boxes *) let v = unbox_typed_value ctx.meta v in let translate = typed_value_to_texpression ctx ectx in (* Translate the type *) let ty = ctx_translate_fwd_ty ctx v.ty in (* Translate the value *) let value = match v.value with | VLiteral cv -> { e = Const cv; ty } | VAdt av -> ( let variant_id = av.variant_id in let field_values = List.map translate av.field_values in (* Eliminate the tuple wrapper if it is a tuple with exactly one field *) match v.ty with | TAdt (TTuple, _) -> sanity_check __FILE__ __LINE__ (variant_id = None) ctx.meta; mk_simpl_tuple_texpression ctx.meta field_values | _ -> (* Retrieve the type and the translated generics from the translated type (simpler this way) *) let adt_id, generics = ty_as_adt ctx.meta ty in (* Create the constructor *) let qualif_id = AdtCons { adt_id; variant_id = av.variant_id } in let qualif = { id = qualif_id; generics } in let cons_e = Qualif qualif in let field_tys = List.map (fun (v : texpression) -> v.ty) field_values in let cons_ty = mk_arrows field_tys ty in let cons = { e = cons_e; ty = cons_ty } in (* Apply the constructor *) mk_apps ctx.meta cons field_values) | VBottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable" | VLoan lc -> ( match lc with | VSharedLoan (_, v) -> translate v | VMutLoan _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable") | VBorrow bc -> ( match bc with | VSharedBorrow bid -> (* Lookup the shared value in the context, and continue *) let sv = InterpreterBorrowsCore.lookup_shared_value ctx.meta ectx bid in translate sv | VReservedMutBorrow bid -> (* Same as for shared borrows. However, note that we use reserved borrows * only in *meta-data*: a value *actually used* in the translation can't come * from an unpromoted reserved borrow *) let sv = InterpreterBorrowsCore.lookup_shared_value ctx.meta ectx bid in translate sv | VMutBorrow (_, v) -> (* Borrows are the identity in the extraction *) translate v) | VSymbolic sv -> symbolic_value_to_texpression ctx sv in (* Debugging *) log#ldebug (lazy ("typed_value_to_texpression: result:" ^ "\n- input value:\n" ^ typed_value_to_string ctx v ^ "\n- translated expression:\n" ^ texpression_to_string ctx value)); (* Sanity check *) type_check_texpression ctx value; (* Return *) value (** Explore an abstraction value and convert it to a consumed value by collecting all the meta-values from the ended *loans*. Consumed values are rvalues because when an abstraction ends we introduce a call to a backward function in the synthesized program, which takes as inputs those consumed values: {[ // Rust: fn choose<'a>(b: bool, x : &'a mut u32, y : &'a mut u32) -> &'a mut u32; // Synthesis: let ... = choose_back b x y nz in ^^ ]} *) let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (av : V.typed_avalue) : texpression option = let translate = typed_avalue_to_consumed ctx ectx in let value = match av.value with | AAdt adt_v -> ( (* Translate the field values *) let field_values = List.filter_map translate adt_v.field_values in (* For now, only tuples can contain borrows *) let adt_id, _ = TypesUtils.ty_as_adt av.ty in match adt_id with | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) -> cassert __FILE__ __LINE__ (field_values = []) ctx.meta "ADTs containing borrows are not supported yet"; None | TTuple -> (* Return *) if field_values = [] then None else (* Note that if there is exactly one field value, * [mk_simpl_tuple_rvalue] is the identity *) let rv = mk_simpl_tuple_texpression ctx.meta field_values in Some rv) | ABottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable" | ALoan lc -> aloan_content_to_consumed ctx ectx lc | ABorrow bc -> aborrow_content_to_consumed ctx bc | ASymbolic aproj -> aproj_to_consumed ctx aproj | AIgnored -> None in (* Sanity check - Rk.: we do this at every recursive call, which is a bit * expansive... *) (match value with | None -> () | Some value -> type_check_texpression ctx value); (* Return *) value and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (lc : V.aloan_content) : texpression option = match lc with | AMutLoan (_, _) | ASharedLoan (_, _, _) -> craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedMutLoan { child = _; given_back = _; given_back_meta } -> (* Return the meta-value *) Some (typed_value_to_texpression ctx ectx given_back_meta) | AEndedSharedLoan (_, _) -> (* We don't dive into shared loans: there is nothing to give back * inside (note that there could be a mutable borrow in the shared * value, pointing to a mutable loan in the child avalue, but this * borrow is in practice immutable) *) None | AIgnoredMutLoan (_, _) -> (* There can be *inner* not ended mutable loans, but not outer ones *) craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedIgnoredMutLoan _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented | AIgnoredSharedLoan _ -> (* Ignore *) None and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) : texpression option = match bc with | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> craise __FILE__ __LINE__ _ctx.meta "Unreachable" | AEndedMutBorrow (_, _) -> (* We collect consumed values: ignore *) None | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented | AEndedSharedBorrow | AProjSharedBorrow _ -> (* Ignore *) None and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option = match aproj with | V.AEndedProjLoans (msv, []) -> (* The symbolic value was left unchanged *) Some (symbolic_value_to_texpression ctx msv) | V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) -> sanity_check __FILE__ __LINE__ (child_aproj = AIgnoredProjBorrows) ctx.meta; (* The symbolic value was updated *) Some (symbolic_value_to_texpression ctx mnv) | V.AEndedProjLoans (_, _) -> (* The symbolic value was updated, and the given back values come from sevearl * abstractions *) raise Unimplemented | AEndedProjBorrows _ -> (* We consider consumed values *) None | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> craise __FILE__ __LINE__ ctx.meta "Unreachable" (** Convert the abstraction values in an abstraction to consumed values. See [typed_avalue_to_consumed]. *) let abs_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (abs : V.abs) : texpression list = log#ldebug (lazy ("abs_to_consumed:\n" ^ abs_to_string ctx abs)); List.filter_map (typed_avalue_to_consumed ctx ectx) abs.avalues let translate_mprojection_elem (pe : E.projection_elem) : mprojection_elem option = match pe with | Deref | DerefBox -> None | Field (pkind, field_id) -> Some { pkind; field_id } let translate_mprojection (p : E.projection) : mprojection = List.filter_map translate_mprojection_elem p (** Translate a "meta"-place *) let translate_mplace (p : S.mplace) : mplace = let var_id = p.bv.index in let name = p.bv.name in let projection = translate_mprojection p.projection in { var_id; name; projection } let translate_opt_mplace (p : S.mplace option) : mplace option = match p with None -> None | Some p -> Some (translate_mplace p) (** Explore an abstraction value and convert it to a given back value by collecting all the meta-values from the ended *borrows*. Given back values are patterns, because when an abstraction ends, we introduce a call to a backward function in the synthesized program, which introduces new values: {[ let (nx, ny) = f_back ... in ^^^^^^^^ ]} [mp]: it is possible to provide some meta-place information, to guide the heuristics which later find pretty names for the variables. *) let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) (ctx : bs_ctx) : bs_ctx * typed_pattern option = let ctx, value = match av.value with | AAdt adt_v -> ( (* Translate the field values *) (* For now we forget the meta-place information so that it doesn't get used * by several fields (which would then all have the same name...), but we * might want to do something smarter *) let mp = None in let ctx, field_values = List.fold_left_map (fun ctx fv -> typed_avalue_to_given_back mp fv ctx) ctx adt_v.field_values in let field_values = List.filter_map (fun x -> x) field_values in (* For now, only tuples can contain borrows - note that if we gave * something like a [&mut Vec] to a function, we give back the * vector value upon visiting the "abstraction borrow" node *) let adt_id, _ = TypesUtils.ty_as_adt av.ty in match adt_id with | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) -> cassert __FILE__ __LINE__ (field_values = []) ctx.meta "ADTs with borrows are not supported yet"; (ctx, None) | TTuple -> (* Return *) let variant_id = adt_v.variant_id in sanity_check __FILE__ __LINE__ (variant_id = None) ctx.meta; if field_values = [] then (ctx, None) else (* Note that if there is exactly one field value, [mk_simpl_tuple_pattern] * is the identity *) let lv = mk_simpl_tuple_pattern field_values in (ctx, Some lv)) | ABottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable" | ALoan lc -> aloan_content_to_given_back mp lc ctx | ABorrow bc -> aborrow_content_to_given_back mp bc ctx | ASymbolic aproj -> aproj_to_given_back mp aproj ctx | AIgnored -> (ctx, None) in (* Sanity check - Rk.: we do this at every recursive call, which is a bit * expansive... *) (match value with None -> () | Some value -> type_check_pattern ctx value); (* Return *) (ctx, value) and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content) (ctx : bs_ctx) : bs_ctx * typed_pattern option = match lc with | AMutLoan (_, _) | ASharedLoan (_, _, _) -> craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedMutLoan { child = _; given_back = _; given_back_meta = _ } | AEndedSharedLoan (_, _) -> (* We consider given back values, and thus ignore those *) (ctx, None) | AIgnoredMutLoan (_, _) -> (* There can be *inner* not ended mutable loans, but not outer ones *) craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedIgnoredMutLoan _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented | AIgnoredSharedLoan _ -> (* Ignore *) (ctx, None) and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content) (ctx : bs_ctx) : bs_ctx * typed_pattern option = match bc with | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedMutBorrow (msv, _) -> (* Return the meta-symbolic-value *) let ctx, var = fresh_var_for_symbolic_value msv ctx in (ctx, Some (mk_typed_pattern_from_var var mp)) | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented | AEndedSharedBorrow | AProjSharedBorrow _ -> (* Ignore *) (ctx, None) and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : bs_ctx * typed_pattern option = match aproj with | V.AEndedProjLoans (_, child_projs) -> (* There may be children borrow projections in case of nested borrows, * in which case we need to dive in - we disallow nested borrows for now *) cassert __FILE__ __LINE__ (List.for_all (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows) child_projs) ctx.meta "Nested borrows are not supported yet"; (ctx, None) | AEndedProjBorrows mv -> (* Return the meta-value *) let ctx, var = fresh_var_for_symbolic_value mv ctx in (ctx, Some (mk_typed_pattern_from_var var mp)) | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> craise __FILE__ __LINE__ ctx.meta "Unreachable" (** Convert the abstraction values in an abstraction to given back values. See [typed_avalue_to_given_back]. *) let abs_to_given_back (mpl : mplace option list option) (abs : V.abs) (ctx : bs_ctx) : bs_ctx * typed_pattern list = let avalues = match mpl with | None -> List.map (fun av -> (None, av)) abs.avalues | Some mpl -> List.combine mpl abs.avalues in let ctx, values = List.fold_left_map (fun ctx (mp, av) -> typed_avalue_to_given_back mp av ctx) ctx avalues in let values = List.filter_map (fun x -> x) values in (ctx, values) (** Simply calls [abs_to_given_back] *) let abs_to_given_back_no_mp (abs : V.abs) (ctx : bs_ctx) : bs_ctx * typed_pattern list = let mpl = List.map (fun _ -> None) abs.avalues in abs_to_given_back (Some mpl) abs ctx (** Return the ordered list of the (transitive) parents of a given abstraction. Is used for instance when collecting the input values given to all the parent functions, in order to properly instantiate an *) let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) : S.call * (V.abs * texpression list) list = let call_info = V.FunCallId.Map.find call_id ctx.calls in let abs_ancestors = list_ancestor_abstractions ctx abs call_id in (call_info.forward, abs_ancestors) (** Add meta-information to an expression *) let mk_emeta_symbolic_assignments (vars : var list) (values : texpression list) (e : texpression) : texpression = let var_values = List.combine (List.map var_get_id vars) values in if var_values <> [] then mk_emeta (SymbolicAssignments var_values) e else e (** Derive naming information from a context. We explore the context and look in which bindings the symbolic values appear: we use this information to derive naming information. *) let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx) (ectx : Contexts.eval_ctx) : (VarId.id * string) list = let info : (VarId.id * string) list ref = ref [] in let push_info name sv = info := (name, sv) :: !info in let visitor = object (self) inherit [_] Contexts.iter_eval_ctx method! visit_env_elem _ ee = match ee with | EBinding (BVar { index = _; name = Some name }, v) -> self#visit_typed_value name v | _ -> () (* Ignore *) method! visit_value name v = match v with | VLiteral _ | VBottom -> () | VBorrow (VMutBorrow (_, v)) | VLoan (VSharedLoan (_, v)) -> self#visit_typed_value name v | VSymbolic sv -> (* Translate the type *) let ty = ctx_translate_fwd_ty ctx sv.sv_ty in (* If the type is unit, do nothing *) if ty_is_unit ty then () else (* Otherwise lookup the variable *) let var = lookup_var_for_symbolic_value sv ctx in push_info var.id name | _ -> () end in (* Visit the context *) visitor#visit_eval_ctx "x" ectx; (* Return the computed information *) !info let translate_error (meta : Meta.meta option) (msg : string) : texpression = { e = EError (meta, msg); ty = Error } let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = match e with | S.Return (ectx, opt_v) -> (* We reached a return. Remark: we can't get there if we are inside a loop. *) translate_return ectx opt_v ctx | ReturnWithLoop (loop_id, is_continue) -> (* We reached a return and are inside a loop. *) translate_return_with_loop loop_id is_continue ctx | Panic -> translate_panic ctx | FunCall (call, e) -> translate_function_call call e ctx | EndAbstraction (ectx, abs, e) -> translate_end_abstraction ectx abs e ctx | EvalGlobal (gid, generics, sv, e) -> translate_global_eval gid generics sv e ctx | Assertion (ectx, v, e) -> translate_assertion ectx v e ctx | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx | IntroSymbolic (ectx, p, sv, v, e) -> translate_intro_symbolic ectx p sv v e ctx | Meta (meta, e) -> translate_emeta meta e ctx | ForwardEnd (ectx, loop_input_values, e, back_e) -> (* Translate the end of a function, or the end of a loop. The case where we (re-)enter a loop is handled here. *) translate_forward_end ectx loop_input_values e back_e ctx | Loop loop -> translate_loop loop ctx | Error (meta, msg) -> translate_error meta msg and translate_panic (ctx : bs_ctx) : texpression = (* Here we use the function return type - note that it is ok because * we don't match on panics which happen inside the function body - * but it won't be true anymore once we translate individual blocks *) (* If we use a state monad, we need to add a lambda for the state variable *) (* Note that only forward functions return a state *) let effect_info = ctx_get_effect_info ctx in (* TODO: we should use a [Fail] function *) let mk_output output_ty = if effect_info.stateful then (* Create the [Fail] value *) let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in let ret_v = mk_result_fail_texpression_with_error_id ctx.meta error_failure_id ret_ty in ret_v else mk_result_fail_texpression_with_error_id ctx.meta error_failure_id output_ty in if ctx.inside_loop && Option.is_some ctx.bid then (* We are synthesizing the backward function of a loop body *) let bid = Option.get ctx.bid in let loop_id = Option.get ctx.loop_id in let loop = LoopId.Map.find loop_id ctx.loops in let tys = RegionGroupId.Map.find bid loop.back_outputs in let output = mk_simpl_tuple_ty tys in mk_output output else (* Regular function, or forward function (the forward translation for a loop has the same return type as the parent function) *) match ctx.bid with | None -> let back_tys = compute_back_tys ctx.sg None in let back_tys = List.filter_map (fun x -> x) back_tys in let tys = if ctx.sg.fwd_info.ignore_output then back_tys else ctx.sg.fwd_output :: back_tys in let output = mk_simpl_tuple_ty tys in mk_output output | Some bid -> let output = mk_simpl_tuple_ty (RegionGroupId.Map.find bid ctx.sg.back_sg).outputs in mk_output output (** [opt_v]: the value to return, in case we translate a forward body. Remark: for now, we can't get there if we are inside a loop. If inside a loop, we use {!translate_return_with_loop}. Remark: in case we merge the forward/backward functions, we introduce those in [translate_forward_end]. *) and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option) (ctx : bs_ctx) : texpression = (* There are two cases: - either we reach the return of a forward function or a forward loop body, in which case the optional value should be [Some] (it is the returned value) - or we are translating a backward function, in which case it should be [None] *) (* Compute the values that we should return *without the state and the result wrapper* *) let output = match ctx.bid with | None -> (* Forward function *) let v = Option.get opt_v in typed_value_to_texpression ctx ectx v | Some _ -> (* Backward function *) (* Sanity check *) sanity_check __FILE__ __LINE__ (opt_v = None) ctx.meta; (* Group the variables in which we stored the values we need to give back. See the explanations for the [SynthInput] case in [translate_end_abstraction] *) let backward_outputs = Option.get ctx.backward_outputs in let field_values = List.map mk_texpression_from_var backward_outputs in mk_simpl_tuple_texpression ctx.meta field_values in (* We may need to return a state * - error-monad: Return x * - state-error: Return (state, x) * *) let effect_info = ctx_get_effect_info ctx in let output = if effect_info.stateful then let state_rvalue = mk_state_texpression ctx.state_var in mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ] else output in (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *) mk_result_return_texpression ctx.meta output and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) (ctx : bs_ctx) : texpression = sanity_check __FILE__ __LINE__ (is_continue = ctx.inside_loop) ctx.meta; let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in sanity_check __FILE__ __LINE__ (loop_id = Option.get ctx.loop_id) ctx.meta; (* Lookup the loop information *) let loop_id = Option.get ctx.loop_id in let loop_info = LoopId.Map.find loop_id ctx.loops in (* There are two cases depending on whether we translate a backward function or not. *) let output = match ctx.bid with | None -> Option.get loop_info.forward_output_no_state_no_result | Some _ -> (* Backward *) (* Group the variables in which we stored the values we need to give back. * See the explanations for the [SynthInput] case in [translate_end_abstraction] *) (* It can happen that we did not end any output abstraction, because the loop didn't use borrows corresponding to the region we just ended. If this happens, there are no backward outputs. *) let backward_outputs = match ctx.backward_outputs with Some outputs -> outputs | None -> [] in let field_values = List.map mk_texpression_from_var backward_outputs in mk_simpl_tuple_texpression ctx.meta field_values in (* We may need to return a state * - error-monad: Return x * - state-error: Return (state, x) * Note that the loop function and the parent function live in the same * effect - in particular, one manipulates a state iff the other does * the same. * *) let effect_info = ctx_get_effect_info ctx in let output = if effect_info.stateful then let state_rvalue = mk_state_texpression ctx.state_var in mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ] else output in (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *) mk_emeta (Tag "return_with_loop") (mk_result_return_texpression ctx.meta output) and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : texpression = log#ldebug (lazy ("translate_function_call:\n" ^ "\n- call.call_id:" ^ S.show_call_id call.call_id ^ "\n\n- call.generics:\n" ^ ctx_generic_args_to_string ctx call.generics)); (* Translate the function call *) let generics = ctx_translate_fwd_generic_args ctx call.generics in let args = let args = List.map (typed_value_to_texpression ctx call.ctx) call.args in let args_mplaces = List.map translate_opt_mplace call.args_places in List.map (fun (arg, mp) -> mk_opt_mplace_texpression mp arg) (List.combine args args_mplaces) in let dest_mplace = translate_opt_mplace call.dest_place in (* Retrieve the function id, and register the function call in the context * if necessary. *) let ctx, fun_id, effect_info, args, dest_v = match call.call_id with | S.Fun (fid, call_id) -> (* Regular function call *) let fid_t = translate_fun_id_or_trait_method_ref ctx fid in let func = Fun (FromLlbc (fid_t, None)) in (* Retrieve the effect information about this function (can fail, * takes a state as input, etc.) *) let effect_info = get_fun_effect_info ctx fid None None in (* Depending on the function effects: - add the fuel - add the state input argument - generate a fresh state variable for the returned state *) let args, ctx, out_state = let fuel = mk_fuel_input_as_list ctx effect_info in if effect_info.stateful then let state_var = mk_state_texpression ctx.state_var in let ctx, _, nstate_var = bs_ctx_fresh_state_var ctx in (List.concat [ fuel; args; [ state_var ] ], ctx, Some nstate_var) else (List.concat [ fuel; args ], ctx, None) in (* Generate the variables for the backward functions returned by the forward function. *) let ctx, ignore_fwd_output, back_funs_map, back_funs = (* We need to compute the signatures of the backward functions. *) let sg = Option.get call.sg in let decls_ctx = ctx.decls_ctx in let dsg = translate_fun_sig_with_regions_hierarchy_to_decomposed ctx.meta decls_ctx fid call.regions_hierarchy sg (List.map (fun _ -> None) sg.inputs) in log#ldebug (lazy ("dsg.generics:\n" ^ show_generic_params dsg.generics)); let tr_self, all_generics = match call.trait_method_generics with | None -> (UnknownTrait __FUNCTION__, generics) | Some (all_generics, tr_self) -> let all_generics = ctx_translate_fwd_generic_args ctx all_generics in let tr_self = translate_fwd_trait_instance_id ctx.meta ctx.type_ctx.type_infos tr_self in (tr_self, all_generics) in let back_tys = compute_back_tys_with_info dsg (Some (all_generics, tr_self)) in (* Introduce variables for the backward functions *) (* Compute a proper basename for the variables *) let back_fun_name = let name = match fid with | FunId (FAssumed fid) -> ( match fid with | BoxNew -> "box_new" | BoxFree -> "box_free" | ArrayRepeat -> "array_repeat" | ArrayIndexShared -> "index_shared" | ArrayIndexMut -> "index_mut" | ArrayToSliceShared -> "to_slice_shared" | ArrayToSliceMut -> "to_slice_mut" | SliceIndexShared -> "index_shared" | SliceIndexMut -> "index_mut") | FunId (FRegular fid) | TraitMethod (_, _, fid) -> ( let decl = FunDeclId.Map.find fid ctx.fun_ctx.llbc_fun_decls in match Collections.List.last decl.name with | PeIdent (s, _) -> s | PeImpl _ -> (* We shouldn't get there *) craise __FILE__ __LINE__ decl.meta "Unexpected") in name ^ "_back" in let ctx, back_vars = fresh_opt_vars (List.map (fun ty -> match ty with | None -> None | Some (back_sg, ty) -> (* We insert a name for the variable only if the function can fail: if it can fail, it means the call returns a backward function. Otherwise, it directly returns the value given back by the backward function, which means we shouldn't give it a name like "back..." (it doesn't make sense) *) let name = if back_sg.effect_info.can_fail then Some back_fun_name else None in Some (name, ty)) back_tys) ctx in let back_funs = List.filter_map (fun v -> match v with | None -> None | Some v -> Some (mk_typed_pattern_from_var v None)) back_vars in let gids = List.map (fun (g : T.region_var_group) -> g.id) call.regions_hierarchy in let back_vars = List.map (Option.map mk_texpression_from_var) back_vars in let back_funs_map = RegionGroupId.Map.of_list (List.combine gids back_vars) in (ctx, dsg.fwd_info.ignore_output, Some back_funs_map, back_funs) in (* Compute the pattern for the destination *) let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in let dest = (* Here there is something subtle: as we might ignore the output of the forward function (because it translates to unit) we doNOT necessarily introduce in the let-binding the variable to which we map the symbolic value which was introduced for the output of the function call. This would be problematic if later we need to translate this symbolic value, but we implemented {!symbolic_value_to_texpression} so that it doesn't perform any lookups if the symbolic value has type unit. *) let vars = if ignore_fwd_output then back_funs else dest :: back_funs in mk_simpl_tuple_pattern vars in let dest = match out_state with | None -> dest | Some out_state -> mk_simpl_tuple_pattern [ out_state; dest ] in (* Register the function call *) let ctx = bs_ctx_register_forward_call call_id call args back_funs_map ctx in (ctx, func, effect_info, args, dest) | S.Unop E.Not -> let effect_info = { can_fail = false; stateful_group = false; stateful = false; can_diverge = false; is_rec = false; } in let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop Not, effect_info, args, dest) | S.Unop E.Neg -> ( match args with | [ arg ] -> let int_ty = ty_as_integer ctx.meta arg.ty in (* Note that negation can lead to an overflow and thus fail (it * is thus monadic) *) let effect_info = { can_fail = true; stateful_group = false; stateful = false; can_diverge = false; is_rec = false; } in let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop (Neg int_ty), effect_info, args, dest) | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable") | S.Unop (E.Cast cast_kind) -> ( match cast_kind with | CastScalar (src_ty, tgt_ty) -> (* Note that cast can fail *) let effect_info = { can_fail = true; stateful_group = false; stateful = false; can_diverge = false; is_rec = false; } in let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, dest) | CastFnPtr _ -> craise __FILE__ __LINE__ ctx.meta "TODO: function casts") | S.Binop binop -> ( match args with | [ arg0; arg1 ] -> let int_ty0 = ty_as_integer ctx.meta arg0.ty in let int_ty1 = ty_as_integer ctx.meta arg1.ty in (match binop with (* The Rust compiler accepts bitshifts for any integer type combination for ty0, ty1 *) | E.Shl | E.Shr -> () | _ -> sanity_check __FILE__ __LINE__ (int_ty0 = int_ty1) ctx.meta); let effect_info = { can_fail = ExpressionsUtils.binop_can_fail binop; stateful_group = false; stateful = false; can_diverge = false; is_rec = false; } in let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Binop (binop, int_ty0), effect_info, args, dest) | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable") in let func = { id = FunOrOp fun_id; generics } in let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in let ret_ty = if effect_info.can_fail then mk_result_ty dest_v.ty else dest_v.ty in let func_ty = mk_arrows input_tys ret_ty in let func = { e = Qualif func; ty = func_ty } in let call = mk_apps ctx.meta func args in (* Translate the next expression *) let next_e = translate_expression e ctx in (* Put together *) mk_let effect_info.can_fail dest_v call next_e and translate_end_abstraction (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : texpression = log#ldebug (lazy ("translate_end_abstraction: abstraction kind: " ^ V.show_abs_kind abs.kind)); match abs.kind with | V.SynthInput rg_id -> translate_end_abstraction_synth_input ectx abs e ctx rg_id | V.FunCall (call_id, rg_id) -> translate_end_abstraction_fun_call ectx abs e ctx call_id rg_id | V.SynthRet rg_id -> translate_end_abstraction_synth_ret ectx abs e ctx rg_id | V.Loop (loop_id, rg_id, abs_kind) -> translate_end_abstraction_loop ectx abs e ctx loop_id rg_id abs_kind | V.Identity -> translate_end_abstraction_identity ectx abs e ctx and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) (rg_id : T.RegionGroupId.id) : texpression = log#ldebug (lazy ("translate_end_abstraction_synth_input:" ^ "\n- function: " ^ name_to_string ctx ctx.fun_decl.name ^ "\n- rg_id: " ^ T.RegionGroupId.to_string rg_id ^ "\n- loop_id: " ^ Print.option_to_string Pure.LoopId.to_string ctx.loop_id ^ "\n- eval_ctx:\n" ^ eval_ctx_to_string ~meta:(Some ctx.meta) ectx ^ "\n- abs:\n" ^ abs_to_string ctx abs ^ "\n")); (* When we end an input abstraction, this input abstraction gets back the borrows which it introduced in the context through the input values: by listing those values, we get the values which are given back by one of the backward functions we are synthesizing. Note that we don't support nested borrows for now: if we find an ended synthesized input abstraction, it must be the one corresponding to the backward function wer are synthesizing, it can't be the one for a parent backward function. *) let bid = Option.get ctx.bid in sanity_check __FILE__ __LINE__ (rg_id = bid) ctx.meta; (* First, introduce the given back variables. We don't use the same given back variables if we translate a loop or the standard body of a function. *) let ctx, given_back_variables = let vars = if ctx.inside_loop then (* We are synthesizing a loop body *) let loop_id = Option.get ctx.loop_id in let loop = LoopId.Map.find loop_id ctx.loops in let tys = RegionGroupId.Map.find bid loop.back_outputs in List.map (fun ty -> (None, ty)) tys else (* Regular function body *) let back_sg = RegionGroupId.Map.find bid ctx.sg.back_sg in List.combine back_sg.output_names back_sg.outputs in let ctx, vars = fresh_vars vars ctx in ({ ctx with backward_outputs = Some vars }, vars) in (* Get the list of values consumed by the abstraction upon ending *) let consumed_values = abs_to_consumed ctx ectx abs in log#ldebug (lazy ("translate_end_abstraction_synth_input:" ^ "\n\n- given back variables types:\n" ^ Print.list_to_string (fun (v : var) -> pure_ty_to_string ctx v.ty) given_back_variables ^ "\n\n- consumed values:\n" ^ Print.list_to_string (fun e -> texpression_to_string ctx e ^ " : " ^ pure_ty_to_string ctx e.ty) consumed_values ^ "\n")); (* Group the two lists *) let variables_values = List.combine given_back_variables consumed_values in (* Sanity check: the two lists match (same types) *) (* TODO: normalize the types *) if !Config.type_check_pure_code then List.iter (fun (var, v) -> sanity_check __FILE__ __LINE__ ((var : var).ty = (v : texpression).ty) ctx.meta) variables_values; (* Translate the next expression *) let next_e = translate_expression e ctx in (* Generate the assignemnts *) let monadic = false in List.fold_right (fun (var, value) (e : texpression) -> mk_let monadic (mk_typed_pattern_from_var var None) value e) variables_values next_e and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) (call_id : V.FunCallId.id) (rg_id : T.RegionGroupId.id) : texpression = let call_info = V.FunCallId.Map.find call_id ctx.calls in let call = call_info.forward in let fun_id = match call.call_id with | S.Fun (fun_id, _) -> fun_id | Unop _ | Binop _ -> (* Those don't have backward functions *) craise __FILE__ __LINE__ ctx.meta "Unreachable" in let effect_info = get_fun_effect_info ctx fun_id None (Some rg_id) in (* Retrieve the values consumed upon ending the loans inside this * abstraction: those give us the remaining input values *) let back_inputs = abs_to_consumed ctx ectx abs in (* If the function is stateful: * - add the state input argument * - generate a fresh state variable for the returned state *) let back_state, ctx, nstate = if effect_info.stateful then let back_state = mk_state_texpression ctx.state_var in let ctx, _, nstate = bs_ctx_fresh_state_var ctx in ([ back_state ], ctx, Some nstate) else ([], ctx, None) in let back_inputs = List.append back_inputs back_state in (* Retrieve the values given back by this function: those are the output * values. We rely on the fact that there are no nested borrows to use the * meta-place information from the input values given to the forward function * (we need to add [None] for the return avalue) *) let output_mpl = List.append (List.map translate_opt_mplace call.args_places) [ None ] in let ctx, outputs = abs_to_given_back (Some output_mpl) abs ctx in (* Group the output values together: first the updated inputs *) let output = mk_simpl_tuple_pattern outputs in (* Add the returned state if the function is stateful *) let output = match nstate with | None -> output | Some nstate -> mk_simpl_tuple_pattern [ nstate; output ] in (* Retrieve the function id, and register the function call in the context if necessary.Arith_status *) let ctx, func = bs_ctx_register_backward_call abs call_id rg_id back_inputs ctx in (* Translate the next expression *) let next_e = translate_expression e ctx in (* Put everything together *) let inputs = back_inputs in let args_mplaces = List.map (fun _ -> None) inputs in let args = List.map (fun (arg, mp) -> mk_opt_mplace_texpression mp arg) (List.combine inputs args_mplaces) in (* The backward function might have been filtered it does nothing (consumes unit and returns unit). *) match func with | None -> next_e | Some func -> log#ldebug (lazy (let args = List.map (texpression_to_string ctx) args in "func: " ^ texpression_to_string ctx func ^ "\nfunc type: " ^ pure_ty_to_string ctx func.ty ^ "\n\nargs:\n" ^ String.concat "\n" args)); let call = mk_apps ctx.meta func args in mk_let effect_info.can_fail output call next_e and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : texpression = (* We simply check that the abstraction only contains shared borrows/loans, and translate the next expression *) (* We can do this simply by checking that it consumes and gives back nothing *) let inputs = abs_to_consumed ctx ectx abs in let ctx, outputs = abs_to_given_back None abs ctx in sanity_check __FILE__ __LINE__ (inputs = []) ctx.meta; sanity_check __FILE__ __LINE__ (outputs = []) ctx.meta; (* Translate the next expression *) translate_expression e ctx and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) (rg_id : T.RegionGroupId.id) : texpression = (* If we end the abstraction which consumed the return value of the function we are synthesizing, we get back the borrows which were inside. Those borrows are actually input arguments of the backward function we are synthesizing. So we simply need to introduce proper let bindings. For instance: {[ fn id<'a>(x : &'a mut u32) -> &'a mut u32 { x } ]} Upon ending the return abstraction for 'a, we get back the borrow for [x]. This new value is the second argument of the backward function: {[ let id_back x nx = nx ]} In practice, upon ending this abstraction we introduce a useless let-binding: {[ let id_back x nx = let s = nx in // the name [s] is not important (only collision matters) ... ]} This let-binding later gets inlined, during a micro-pass. *) (* First, retrieve the list of variables used for the inputs for the * backward function *) let inputs = T.RegionGroupId.Map.find rg_id ctx.backward_inputs_no_state in (* Retrieve the values consumed upon ending the loans inside this * abstraction: as there are no nested borrows, there should be none. *) let consumed = abs_to_consumed ctx ectx abs in cassert __FILE__ __LINE__ (consumed = []) ctx.meta "Nested borrows are not supported yet"; (* Retrieve the values given back upon ending this abstraction - note that * we don't provide meta-place information, because those assignments will * be inlined anyway... *) log#ldebug (lazy ("abs: " ^ abs_to_string ctx abs)); let ctx, given_back = abs_to_given_back_no_mp abs ctx in (* Link the inputs to those given back values - note that this also * checks we have the same number of values, of course *) let given_back_inputs = List.combine given_back inputs in (* Sanity check *) List.iter (fun ((given_back, input) : typed_pattern * var) -> log#ldebug (lazy ("\n- given_back ty: " ^ pure_ty_to_string ctx given_back.ty ^ "\n- sig input ty: " ^ pure_ty_to_string ctx input.ty)); sanity_check __FILE__ __LINE__ (given_back.ty = input.ty) ctx.meta) given_back_inputs; (* Translate the next expression *) let next_e = translate_expression e ctx in (* Generate the assignments *) let monadic = false in List.fold_right (fun (given_back, input_var) e -> mk_let monadic given_back (mk_texpression_from_var input_var) e) given_back_inputs next_e and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) (loop_id : V.LoopId.id) (rg_id : T.RegionGroupId.id option) (abs_kind : V.loop_abs_kind) : texpression = let vloop_id = loop_id in let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in sanity_check __FILE__ __LINE__ (loop_id = Option.get ctx.loop_id) ctx.meta; let rg_id = Option.get rg_id in (* There are two cases depending on the [abs_kind] (whether this is a synth input or a regular loop call) *) match abs_kind with | V.LoopSynthInput -> (* Actually the same case as [SynthInput] *) translate_end_abstraction_synth_input ectx abs e ctx rg_id | V.LoopCall -> ( (* We need to introduce a call to the backward function corresponding to a forward call which happened earlier *) let fun_id = E.FRegular ctx.fun_decl.def_id in let effect_info = get_fun_effect_info ctx (FunId fun_id) (Some vloop_id) (Some rg_id) in let loop_info = LoopId.Map.find loop_id ctx.loops in (* Retrieve the additional backward inputs. Note that those are actually the backward inputs of the function we are synthesizing (and that we need to *transmit* to the loop backward function): they are not the values consumed upon ending the abstraction (i.e., we don't use [abs_to_consumed]) *) let back_inputs_vars = T.RegionGroupId.Map.find rg_id ctx.backward_inputs_no_state in let back_inputs = List.map mk_texpression_from_var back_inputs_vars in (* If the function is stateful: * - add the state input argument * - generate a fresh state variable for the returned state *) let back_state, ctx, nstate = if effect_info.stateful then let back_state = mk_state_texpression ctx.state_var in let ctx, _, nstate = bs_ctx_fresh_state_var ctx in ([ back_state ], ctx, Some nstate) else ([], ctx, None) in (* Concatenate all the inputs *) let inputs = List.concat [ back_inputs; back_state ] in (* Retrieve the values given back by this function *) let ctx, outputs = abs_to_given_back None abs ctx in (* Group the output values together: first the updated inputs *) let output = mk_simpl_tuple_pattern outputs in (* Add the returned state if the function is stateful *) let output = match nstate with | None -> output | Some nstate -> mk_simpl_tuple_pattern [ nstate; output ] in (* Translate the next expression *) let next_e = translate_expression e ctx in (* Put everything together *) let args_mplaces = List.map (fun _ -> None) inputs in let args = List.map (fun (arg, mp) -> mk_opt_mplace_texpression mp arg) (List.combine inputs args_mplaces) in (* Create the expression for the function: - it is either a call to a top-level function, if we split the forward/backward functions - or a call to the variable we introduced for the backward function, if we merge the forward/backward functions *) let func = RegionGroupId.Map.find rg_id (Option.get loop_info.back_funs) in (* We may have filtered the backward function elsewhere if it doesn't do anything (doesn't consume anything and doesn't return anything) *) match func with | None -> next_e | Some func -> let call = mk_apps ctx.meta func args in (* Add meta-information - this is slightly hacky: we look at the values consumed by the abstraction (note that those come from *before* we applied the fixed-point context) and use them to guide the naming of the output vars. Also, we need to convert the backward outputs from patterns to variables. Finally, in practice, this works well only for loop bodies: we do this only in this case. TODO: improve the heuristics, to give weight to the hints for instance. *) let next_e = if ctx.inside_loop then let consumed_values = abs_to_consumed ctx ectx abs in let var_values = List.combine outputs consumed_values in let var_values = List.filter_map (fun (var, v) -> match var.Pure.value with | PatVar (var, _) -> Some (var, v) | _ -> None) var_values in let vars, values = List.split var_values in mk_emeta_symbolic_assignments vars values next_e else next_e in (* Create the let-binding *) mk_let effect_info.can_fail output call next_e) and translate_global_eval (gid : A.GlobalDeclId.id) (generics : T.generic_args) (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) : texpression = let ctx, var = fresh_var_for_symbolic_value sval ctx in let decl = A.GlobalDeclId.Map.find gid ctx.global_ctx.llbc_global_decls in let generics = ctx_translate_fwd_generic_args ctx generics in let global_expr = { id = Global gid; generics } in (* We use translate_fwd_ty to translate the global type *) let ty = ctx_translate_fwd_ty ctx decl.ty in let gval = { e = Qualif global_expr; ty } in let e = translate_expression e ctx in mk_let false (mk_typed_pattern_from_var var None) gval e and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value) (e : S.expression) (ctx : bs_ctx) : texpression = let next_e = translate_expression e ctx in let monadic = true in let v = typed_value_to_texpression ctx ectx v in let args = [ v ] in let func = { id = FunOrOp (Fun (Pure Assert)); generics = empty_generic_args } in let func_ty = mk_arrow (TLiteral TBool) mk_unit_ty in let func = { e = Qualif func; ty = func_ty } in let assertion = mk_apps ctx.meta func args in mk_let monadic (mk_dummy_pattern mk_unit_ty) assertion next_e and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) (exp : S.expansion) (ctx : bs_ctx) : texpression = (* Translate the scrutinee *) let scrutinee = symbolic_value_to_texpression ctx sv in let scrutinee_mplace = translate_opt_mplace p in (* Translate the branches *) match exp with | ExpandNoBranch (sexp, e) -> ( match sexp with | V.SeLiteral _ -> (* We do not *register* symbolic expansions to literal values in the symbolic ADT *) craise __FILE__ __LINE__ ctx.meta "Unreachable" | SeMutRef (_, nsv) | SeSharedRef (_, nsv) -> (* The (mut/shared) borrow type is extracted to identity: we thus simply introduce an reassignment *) let ctx, var = fresh_var_for_symbolic_value nsv ctx in let next_e = translate_expression e ctx in let monadic = false in mk_let monadic (mk_typed_pattern_from_var var None) (mk_opt_mplace_texpression scrutinee_mplace scrutinee) next_e | SeAdt _ -> (* Should be in the [ExpandAdt] case *) craise __FILE__ __LINE__ ctx.meta "Unreachable") | ExpandAdt branches -> ( (* We don't do the same thing if there is a branching or not *) match branches with | [] -> craise __FILE__ __LINE__ ctx.meta "Unreachable" | [ (variant_id, svl, branch) ] when not (TypesUtils.ty_is_custom_adt sv.V.sv_ty && !Config.always_deconstruct_adts_with_matches) -> (* There is exactly one branch: no branching. We can decompose the ADT value with a let-binding, unless the backend doesn't support this (see {!Config.always_deconstruct_adts_with_matches}): we *ignore* this branch (and go to the next one) if the ADT is a custom adt, and [always_deconstruct_adts_with_matches] is true. *) translate_ExpandAdt_one_branch sv scrutinee scrutinee_mplace variant_id svl branch ctx | branches -> let translate_branch (variant_id : T.VariantId.id option) (svl : V.symbolic_value list) (branch : S.expression) : match_branch = let ctx, vars = fresh_vars_for_symbolic_values svl ctx in let vars = List.map (fun x -> mk_typed_pattern_from_var x None) vars in let pat_ty = scrutinee.ty in let pat = mk_adt_pattern pat_ty variant_id vars in let branch = translate_expression branch ctx in { pat; branch } in let branches = List.map (fun (vid, svl, e) -> translate_branch vid svl e) branches in let e = Switch ( mk_opt_mplace_texpression scrutinee_mplace scrutinee, Match branches ) in (* There should be at least one branch *) let branch = List.hd branches in let ty = branch.branch.ty in (* Sanity check *) sanity_check __FILE__ __LINE__ (List.for_all (fun br -> br.branch.ty = ty) branches) ctx.meta; (* Return *) { e; ty }) | ExpandBool (true_e, false_e) -> (* We don't need to update the context: we don't introduce any new values/variables *) let true_e = translate_expression true_e ctx in let false_e = translate_expression false_e ctx in let e = Switch ( mk_opt_mplace_texpression scrutinee_mplace scrutinee, If (true_e, false_e) ) in let ty = true_e.ty in log#ldebug (lazy ("true_e.ty: " ^ pure_ty_to_string ctx true_e.ty ^ "\n\nfalse_e.ty: " ^ pure_ty_to_string ctx false_e.ty)); sanity_check __FILE__ __LINE__ (ty = false_e.ty) ctx.meta; { e; ty } | ExpandInt (int_ty, branches, otherwise) -> let translate_branch ((v, branch_e) : V.scalar_value * S.expression) : match_branch = (* We don't need to update the context: we don't introduce any new values/variables *) let branch = translate_expression branch_e ctx in let pat = mk_typed_pattern_from_literal (VScalar v) in { pat; branch } in let branches = List.map translate_branch branches in let otherwise = translate_expression otherwise ctx in let pat_ty = TLiteral (TInteger int_ty) in let otherwise_pat : typed_pattern = { value = PatDummy; ty = pat_ty } in let otherwise : match_branch = { pat = otherwise_pat; branch = otherwise } in let all_branches = List.append branches [ otherwise ] in let e = Switch ( mk_opt_mplace_texpression scrutinee_mplace scrutinee, Match all_branches ) in let ty = otherwise.branch.ty in sanity_check __FILE__ __LINE__ (List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches) ctx.meta; { e; ty } (* Translate and [ExpandAdt] when there is no branching (i.e., one branch). There are several possibilities: - if the ADT is an enumeration, we attempt to deconstruct it with a let-binding: {[ let Cons x0 ... xn = y in ... ]} - if the ADT is a structure, we attempt to introduce one let-binding per field: {[ let x0 = y.f0 in ... let xn = y.fn in ... ]} Of course, this is not always possible depending on the backend. Also, recursive structures, and more specifically structures mutually recursive with inductives, are usually not supported. We define such recursive structures as inductives, in which case it is not always possible to use a notation for the field projections. *) and translate_ExpandAdt_one_branch (sv : V.symbolic_value) (scrutinee : texpression) (scrutinee_mplace : mplace option) (variant_id : variant_id option) (svl : V.symbolic_value list) (branch : S.expression) (ctx : bs_ctx) : texpression = (* TODO: always introduce a match, and use micro-passes to turn the the match into a let? *) let type_id, _ = TypesUtils.ty_as_adt sv.V.sv_ty in let ctx, vars = fresh_vars_for_symbolic_values svl ctx in let branch = translate_expression branch ctx in match type_id with | TAdtId adt_id -> (* Detect if this is an enumeration or not *) let tdef = bs_ctx_lookup_llbc_type_decl adt_id ctx in let is_enum = TypesUtils.type_decl_is_enum tdef in (* We deconstruct the ADT with a single let-binding in two situations: - if the ADT is an enumeration (which must have exactly one branch) - if we forbid using field projectors. *) let is_rec_def = T.TypeDeclId.Set.mem adt_id ctx.type_ctx.recursive_decls in let use_let_with_cons = is_enum || !Config.dont_use_field_projectors (* TODO: for now, we don't have field projectors over recursive ADTs in Lean. *) || (!Config.backend = Lean && is_rec_def) (* Also, there is a special case when the ADT is to be extracted as a tuple, because it is a structure with unnamed fields. Some backends like Lean have projectors for tuples (like so: `x.3`), but others like Coq don't, in which case we have to deconstruct the whole ADT at once (`let (a, b, c) = x in`) *) || TypesUtils.type_decl_from_type_id_is_tuple_struct ctx.type_ctx.type_infos type_id && not (Config.backend_has_tuple_projectors ()) in if use_let_with_cons then (* Introduce a let binding which expands the ADT *) let lvars = List.map (fun v -> mk_typed_pattern_from_var v None) vars in let lv = mk_adt_pattern scrutinee.ty variant_id lvars in let monadic = false in mk_let monadic lv (mk_opt_mplace_texpression scrutinee_mplace scrutinee) branch else (* This is not an enumeration: introduce let-bindings for every * field. * We use the [dest] variable in order not to have to recompute * the type of the result of the projection... *) let adt_id, generics = ty_as_adt ctx.meta scrutinee.ty in let gen_field_proj (field_id : FieldId.id) (dest : var) : texpression = let proj_kind = { adt_id; field_id } in let qualif = { id = Proj proj_kind; generics } in let proj_e = Qualif qualif in let proj_ty = mk_arrow scrutinee.ty dest.ty in let proj = { e = proj_e; ty = proj_ty } in mk_app ctx.meta proj scrutinee in let id_var_pairs = FieldId.mapi (fun fid v -> (fid, v)) vars in let monadic = false in List.fold_right (fun (fid, var) e -> let field_proj = gen_field_proj fid var in mk_let monadic (mk_typed_pattern_from_var var None) field_proj e) id_var_pairs branch | TTuple -> let vars = List.map (fun x -> mk_typed_pattern_from_var x None) vars in let monadic = false in mk_let monadic (mk_simpl_tuple_pattern vars) (mk_opt_mplace_texpression scrutinee_mplace scrutinee) branch | TAssumed TBox -> (* There should be exactly one variable *) let var = match vars with | [ v ] -> v | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable" in (* We simply introduce an assignment - the box type is the * identity when extracted ([box a = a]) *) let monadic = false in mk_let monadic (mk_typed_pattern_from_var var None) (mk_opt_mplace_texpression scrutinee_mplace scrutinee) branch | TAssumed (TArray | TSlice | TStr) -> (* We can't expand those values: we can access the fields only * through the functions provided by the API (note that we don't * know how to expand values like vectors or arrays, because they have a variable number * of fields!) *) craise __FILE__ __LINE__ ctx.meta "Attempt to expand a non-expandable value" and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) (sv : V.symbolic_value) (v : S.value_aggregate) (e : S.expression) (ctx : bs_ctx) : texpression = log#ldebug (lazy ("translate_intro_symbolic:" ^ "\n- value aggregate: " ^ S.show_value_aggregate v)); let mplace = translate_opt_mplace p in (* Introduce a fresh variable for the symbolic value. *) let ctx, var = fresh_var_for_symbolic_value sv ctx in (* Translate the next expression *) let next_e = translate_expression e ctx in (* Translate the value: there are several cases, depending on whether this is a "regular" let-binding, an array aggregate, a const generic or a trait associated constant. *) let v = match v with | VaSingleValue v -> typed_value_to_texpression ctx ectx v | VaArray values -> (* We use a struct update to encode the array aggregate, in order to preserve the structure and allow generating code of the shape `[x0, ...., xn]` *) let values = List.map (typed_value_to_texpression ctx ectx) values in let values = FieldId.mapi (fun fid v -> (fid, v)) values in let su : struct_update = { struct_id = TAssumed TArray; init = None; updates = values } in { e = StructUpdate su; ty = var.ty } | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty } | VaTraitConstValue (trait_ref, const_name) -> let type_infos = ctx.type_ctx.type_infos in let trait_ref = translate_fwd_trait_ref ctx.meta type_infos trait_ref in let qualif_id = TraitConst (trait_ref, const_name) in let qualif = { id = qualif_id; generics = empty_generic_args } in { e = Qualif qualif; ty = var.ty } in (* Make the let-binding *) let monadic = false in let var = mk_typed_pattern_from_var var mplace in mk_let monadic var v next_e and translate_forward_end (ectx : C.eval_ctx) (loop_input_values : V.typed_value S.symbolic_value_id_map option) (fwd_e : S.expression) (back_e : S.expression S.region_group_id_map) (ctx : bs_ctx) : texpression = let translate_one_end ctx (bid : RegionGroupId.id option) = let ctx = { ctx with bid } in (* Update the current state with the additional state received by the backward function, if needs be, and lookup the proper expression *) let ctx, e, finish = match bid with | None -> (* We are translating the forward function - nothing to do *) (ctx, fwd_e, fun e -> e) | Some bid -> (* We need to update the state, and wrap the expression in a lambda, which introduces the additional inputs of the backward function. *) let ctx = (* Introduce variables for the inputs and the state variable and update the context. We need to introduce fresh variables for the additional inputs, because they are locally introduced in a lambda. *) let back_sg = RegionGroupId.Map.find bid ctx.sg.back_sg in let ctx, backward_inputs_no_state = fresh_vars back_sg.inputs_no_state ctx in let ctx, backward_inputs_with_state = if back_sg.effect_info.stateful then let ctx, var, _ = bs_ctx_fresh_state_var ctx in (ctx, backward_inputs_no_state @ [ var ]) else (ctx, backward_inputs_no_state) in { ctx with backward_inputs_no_state = RegionGroupId.Map.add bid backward_inputs_no_state ctx.backward_inputs_no_state; backward_inputs_with_state = RegionGroupId.Map.add bid backward_inputs_with_state ctx.backward_inputs_with_state; } in let e = T.RegionGroupId.Map.find bid back_e in let finish e = (* Wrap in lambdas if necessary *) let inputs = RegionGroupId.Map.find bid ctx.backward_inputs_with_state in let places = List.map (fun _ -> None) inputs in mk_lambdas_from_vars inputs places e in (ctx, e, finish) in let e = translate_expression e ctx in finish e in (* We need to translate the end of the forward function (this is the value we will return) and generate the bodies of the backward functions (which we will also return). Update the current state with the additional state received by the backward function, if needs be, and lookup the proper expression. *) let translate_end ctx = (* Compute the output of the forward function *) let fwd_effect_info = ctx.sg.fwd_info.effect_info in let ctx, pure_fwd_var = fresh_var None ctx.sg.fwd_output ctx in let fwd_e = translate_one_end ctx None in (* If we reached a loop: if we are *inside* a loop, we need to ignore the backward functions which are not associated to region abstractions. *) let keep_rg_ids = match ctx.loop_id with | None -> None | Some loop_id -> if ctx.inside_loop then let loop_info = LoopId.Map.find loop_id ctx.loops in Some (RegionGroupId.Set.of_list (RegionGroupId.Map.keys loop_info.back_outputs)) else None in let keep_rg_id = match keep_rg_ids with | None -> fun _ -> true | Some ids -> fun id -> RegionGroupId.Set.mem id ids in let back_el = List.map (fun ((gid, _) : RegionGroupId.id * back_sg_info) -> if keep_rg_id gid then Some (translate_one_end ctx (Some gid)) else None) (RegionGroupId.Map.bindings ctx.sg.back_sg) in (* Compute whether the backward expressions should be evaluated straight away or not (i.e., if we should bind them with monadic let-bindings or not). We evaluate them straight away if they can fail and have no inputs. *) let evaluate_backs = List.map (fun ((rg_id, sg) : RegionGroupId.id * back_sg_info) -> if keep_rg_id rg_id then Some (if !Config.simplify_merged_fwd_backs then sg.inputs = [] && sg.effect_info.can_fail else false) else None) (RegionGroupId.Map.bindings ctx.sg.back_sg) in (* Introduce variables for the backward functions. We lookup the LLBC definition in an attempt to derive pretty names for those functions. *) let _, back_vars = fresh_back_vars_for_current_fun ctx keep_rg_ids in (* Create the return expressions *) let vars = let back_vars = List.filter_map (fun x -> x) back_vars in if ctx.sg.fwd_info.ignore_output then back_vars else pure_fwd_var :: back_vars in let vars = List.map mk_texpression_from_var vars in let ret = mk_simpl_tuple_texpression ctx.meta vars in (* Introduce a fresh input state variable for the forward expression *) let _ctx, state_var, state_pat = if fwd_effect_info.stateful then let ctx, var, pat = bs_ctx_fresh_state_var ctx in (ctx, [ var ], [ pat ]) else (ctx, [], []) in let state_var = List.map mk_texpression_from_var state_var in let ret = mk_simpl_tuple_texpression ctx.meta (state_var @ [ ret ]) in let ret = mk_result_return_texpression ctx.meta ret in (* Introduce all the let-bindings *) (* Combine: - the backward variables - whether we should evaluate the expression for the backward function (i.e., should we use a monadic let-binding or not - we do if the backward functions don't have inputs and can fail) - the expressions for the backward functions *) let back_vars_els = List.filter_map (fun (v, (eval, el)) -> match v with | None -> None | Some v -> Some (v, Option.get eval, Option.get el)) (List.combine back_vars (List.combine evaluate_backs back_el)) in let e = List.fold_right (fun (var, evaluate, back_e) e -> mk_let evaluate (mk_typed_pattern_from_var var None) back_e e) back_vars_els ret in (* Bind the expression for the forward output *) let fwd_var = mk_typed_pattern_from_var pure_fwd_var None in let pat = mk_simpl_tuple_pattern (state_pat @ [ fwd_var ]) in mk_let fwd_effect_info.can_fail pat fwd_e e in (* If we are (re-)entering a loop, we need to introduce a call to the forward translation of the loop. *) match loop_input_values with | None -> (* "Regular" case: we reached a return *) translate_end ctx | Some loop_input_values -> (* Loop *) let loop_id = Option.get ctx.loop_id in (* Lookup the loop information *) let loop_info = LoopId.Map.find loop_id ctx.loops in log#ldebug (lazy ("translate_forward_end:\n- loop_input_values:\n" ^ V.SymbolicValueId.Map.show (typed_value_to_string ctx) loop_input_values ^ "\n- loop_info.input_svl:\n" ^ Print.list_to_string (symbolic_value_to_string ctx) loop_info.input_svl ^ "\n")); (* Translate the input values *) let loop_input_values = List.map (fun sv -> log#ldebug (lazy ("translate_forward_end: looking up input_svl: " ^ V.SymbolicValueId.to_string sv.V.sv_id ^ "\n")); V.SymbolicValueId.Map.find sv.V.sv_id loop_input_values) loop_info.input_svl in let args = List.map (typed_value_to_texpression ctx ectx) loop_input_values in let org_args = args in (* Lookup the effect info for the loop function *) let fid = E.FRegular ctx.fun_decl.def_id in let effect_info = get_fun_effect_info ctx (FunId fid) None ctx.bid in (* Introduce a fresh output value for the forward function *) let ctx, fwd_output, output_pat = if ctx.sg.fwd_info.ignore_output then (* Note that we still need the forward output (which is unit), because even though the loop function will ignore the forward output, the forward expression will still compute an output (which will have type unit - otherwise we can't ignore it). *) (ctx, mk_unit_rvalue, []) else let ctx, output_var = fresh_var None ctx.sg.fwd_output ctx in ( ctx, mk_texpression_from_var output_var, [ mk_typed_pattern_from_var output_var None ] ) in (* Introduce fresh variables for the backward functions of the loop. For now, the backward functions of the loop are the same as the backward functions of the outer function. *) let ctx, back_funs_map, back_funs = (* We need to filter the region groups which are not linked to region abstractions appearing in the loop, so as not to introduce unnecessary backward functions. *) let keep_rg_ids = RegionGroupId.Set.of_list (RegionGroupId.Map.keys loop_info.back_outputs) in let ctx, back_vars = fresh_back_vars_for_current_fun ctx (Some keep_rg_ids) in let back_funs = List.filter_map (fun v -> match v with | None -> None | Some v -> Some (mk_typed_pattern_from_var v None)) back_vars in let gids = RegionGroupId.Map.keys ctx.sg.back_sg in let back_funs_map = RegionGroupId.Map.of_list (List.combine gids (List.map (Option.map mk_texpression_from_var) back_vars)) in (ctx, Some back_funs_map, back_funs) in (* Introduce patterns *) let args, ctx, out_pats = (* Add the returned backward functions (they might be empty) *) let output_pat = mk_simpl_tuple_pattern (output_pat @ back_funs) in (* Depending on the function effects: * - add the fuel * - add the state input argument * - generate a fresh state variable for the returned state *) let fuel = mk_fuel_input_as_list ctx effect_info in if effect_info.stateful then let state_var = mk_state_texpression ctx.state_var in let ctx, _, nstate_pat = bs_ctx_fresh_state_var ctx in ( List.concat [ fuel; args; [ state_var ] ], ctx, [ nstate_pat; output_pat ] ) else (List.concat [ fuel; args ], ctx, [ output_pat ]) in (* Update the loop information in the context *) let loop_info = { loop_info with forward_inputs = Some args; forward_output_no_state_no_result = Some fwd_output; back_funs = back_funs_map; } in let ctx = { ctx with loops = LoopId.Map.add loop_id loop_info ctx.loops } in (* Translate the end of the function *) let next_e = translate_end ctx in (* Introduce the call to the loop forward function in the generated AST *) let out_pat = mk_simpl_tuple_pattern out_pats in let loop_call = let fun_id = Fun (FromLlbc (FunId fid, Some loop_id)) in let func = { id = FunOrOp fun_id; generics = loop_info.generics } in let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in let ret_ty = if effect_info.can_fail then mk_result_ty out_pat.ty else out_pat.ty in let func_ty = mk_arrows input_tys ret_ty in let func = { e = Qualif func; ty = func_ty } in let call = mk_apps ctx.meta func args in call in (* Create the let expression with the loop call *) let e = mk_let effect_info.can_fail out_pat loop_call next_e in (* Add meta-information linking the loop input parameters and the loop input values - we use this to derive proper names. There is something important here: as we group the end of the function and the loop body in a {!Loop} node, when exploring the function and applying micro passes, we introduce the variables specific to the loop body before exploring both the loop body and the end of the function. It means it is ok to reference some variables which might actually be defined, in the end, in a different branch. We then remove all the meta information from the body *before* calling {!PureMicroPasses.decompose_loops}. *) mk_emeta_symbolic_assignments loop_info.input_vars org_args e and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = let loop_id = V.LoopId.Map.find loop.loop_id ctx.loop_ids_map in (* Translate the loop inputs - some inputs are symbolic values already in the context, some inputs are introduced by the loop fixed point: we need to introduce fresh variables for those. *) (* First introduce fresh variables for the new inputs *) let ctx = (* We have to filter the list of symbolic values, to remove the not fresh ones *) let svl = List.filter (fun (sv : V.symbolic_value) -> V.SymbolicValueId.Set.mem sv.sv_id loop.fresh_svalues) loop.input_svalues in log#ldebug (lazy ("translate_loop:" ^ "\n- input_svalues: " ^ (Print.list_to_string (symbolic_value_to_string ctx)) loop.input_svalues ^ "\n- filtered svl: " ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl ^ "\n- rg_to_abs\n:" ^ T.RegionGroupId.Map.show (Print.list_to_string (ty_to_string ctx)) loop.rg_to_given_back_tys ^ "\n")); let ctx, _ = fresh_vars_for_symbolic_values svl ctx in ctx in (* Sanity check: all the non-fresh symbolic values are in the context *) sanity_check __FILE__ __LINE__ (List.for_all (fun (sv : V.symbolic_value) -> V.SymbolicValueId.Map.mem sv.sv_id ctx.sv_to_var) loop.input_svalues) ctx.meta; (* Translate the loop inputs *) let inputs = List.map (fun sv -> V.SymbolicValueId.Map.find sv.V.sv_id ctx.sv_to_var) loop.input_svalues in let inputs_lvs = List.map (fun var -> mk_typed_pattern_from_var var None) inputs in (* Compute the backward outputs *) let ctx = ref ctx in let rg_to_given_back_tys = RegionGroupId.Map.map (fun tys -> (* The types shouldn't contain borrows - we can translate them as forward types *) List.map (fun ty -> cassert __FILE__ __LINE__ (not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty)) !ctx.meta "The types shouldn't contain borrows"; ctx_translate_fwd_ty !ctx ty) tys) loop.rg_to_given_back_tys in let ctx = !ctx in (* The output type of the loop function *) let fwd_effect_info = { ctx.sg.fwd_info.effect_info with is_rec = true } in let back_effect_infos, output_ty = (* The loop backward functions consume the same additional inputs as the parent function, but have custom outputs *) log#ldebug (lazy (let back_sgs = RegionGroupId.Map.bindings ctx.sg.back_sg in "translate_loop:" ^ "\n- back_sgs: " ^ (Print.list_to_string (Print.pair_to_string RegionGroupId.to_string show_back_sg_info)) back_sgs ^ "\n- given_back_tys: " ^ (RegionGroupId.Map.to_string None (Print.list_to_string (pure_ty_to_string ctx))) rg_to_given_back_tys ^ "\n")); let back_info_tys = List.map (fun ((rg_id, given_back) : RegionGroupId.id * ty list) -> (* Lookup the effect information about the parent function region group associated to this loop region abstraction *) let back_sg = RegionGroupId.Map.find rg_id ctx.sg.back_sg in (* Remark: the effect info of the backward function for the loop is almost the same as for the backward function of the parent function. Quite importantly, the fact that the function is stateful and/or can fail mostly depends on whether it has inputs or not, and the backward functions for the loops have the same inputs as the backward functions for the parent function. *) let effect_info = back_sg.effect_info in let effect_info = { effect_info with is_rec = true } in (* Compute the input/output types *) let inputs = List.map snd back_sg.inputs in let outputs = given_back in (* Filter if necessary *) let ty = if !Config.simplify_merged_fwd_backs && inputs = [] && outputs = [] then None else let output = mk_simpl_tuple_ty outputs in let output = mk_back_output_ty_from_effect_info effect_info inputs output in let ty = mk_arrows inputs output in Some ty in ((rg_id, effect_info), ty)) (RegionGroupId.Map.bindings rg_to_given_back_tys) in let back_info = List.map fst back_info_tys in let back_info = RegionGroupId.Map.of_list back_info in let back_tys = List.filter_map snd back_info_tys in let output = if ctx.sg.fwd_info.ignore_output then back_tys else ctx.sg.fwd_output :: back_tys in let output = mk_simpl_tuple_ty output in let effect_info = ctx.sg.fwd_info.effect_info in let output = if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; output ] else output in let output = if effect_info.can_fail && inputs <> [] then mk_result_ty output else output in (back_info, output) in (* Add the loop information in the context *) let ctx = sanity_check __FILE__ __LINE__ (not (LoopId.Map.mem loop_id ctx.loops)) ctx.meta; (* Note that we will retrieve the input values later in the [ForwardEnd] (and will introduce the outputs at that moment, together with the actual call to the loop forward function) *) let generics = let { types; const_generics; trait_clauses } = ctx.sg.generics in let types = List.map (fun (ty : T.type_var) -> TVar ty.T.index) types in let const_generics = List.map (fun (cg : T.const_generic_var) -> T.CgVar cg.T.index) const_generics in let trait_refs = List.map (fun (c : trait_clause) -> let trait_decl_ref = { trait_decl_id = c.trait_id; decl_generics = empty_generic_args } in { trait_id = Clause c.clause_id; generics = empty_generic_args; trait_decl_ref; }) trait_clauses in { types; const_generics; trait_refs } in let loop_info = { loop_id; input_vars = inputs; input_svl = loop.input_svalues; generics; forward_inputs = None; forward_output_no_state_no_result = None; back_outputs = rg_to_given_back_tys; back_funs = None; fwd_effect_info; back_effect_infos; } in let loops = LoopId.Map.add loop_id loop_info ctx.loops in { ctx with loops } in (* Update the context to translate the function end *) let ctx_end = { ctx with loop_id = Some loop_id } in let fun_end = translate_expression loop.end_expr ctx_end in (* Update the context for the loop body *) let ctx_loop = { ctx_end with inside_loop = true } in (* Add the input state *) let input_state = if (ctx_get_effect_info ctx).stateful then Some ctx.state_var else None in (* Translate the loop body *) let loop_body = translate_expression loop.loop_expr ctx_loop in (* Create the loop node and return *) let loop = Loop { fun_end; loop_id; meta = loop.meta; fuel0 = ctx.fuel0; fuel = ctx.fuel; input_state; inputs; inputs_lvs; output_ty; loop_body; } in let ty = fun_end.ty in { e = loop; ty } and translate_emeta (meta : S.emeta) (e : S.expression) (ctx : bs_ctx) : texpression = let next_e = translate_expression e ctx in let meta = match meta with | S.Assignment (ectx, lp, rv, rp) -> let lp = translate_mplace lp in let rv = typed_value_to_texpression ctx ectx rv in let rp = translate_opt_mplace rp in Some (Assignment (lp, rv, rp)) | S.Snapshot ectx -> let infos = eval_ctx_to_symbolic_assignments_info ctx ectx in if infos <> [] then (* If often happens that the next expression contains exactly the same meta information *) match next_e.e with | Meta (SymbolicPlaces infos1, _) when infos1 = infos -> None | _ -> Some (SymbolicPlaces infos) else None in match meta with | Some meta -> let e = Meta (meta, next_e) in let ty = next_e.ty in { e; ty } | None -> next_e (** Wrap a function body in a match over the fuel to control termination. *) let wrap_in_match_fuel (meta : Meta.meta) (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression) : texpression = let fuel0_var : var = mk_fuel_var fuel0 in let fuel0 = mk_texpression_from_var fuel0_var in let nfuel_var : var = mk_fuel_var fuel in let nfuel_pat = mk_typed_pattern_from_var nfuel_var None in let fail_branch = mk_result_fail_texpression_with_error_id meta error_out_of_fuel_id body.ty in match !Config.backend with | FStar -> (* Generate an expression: {[ if fuel0 = 0 then Fail OutOfFuel else let fuel = decrease fuel0 in ... }] *) (* Create the expression: [fuel0 = 0] *) let check_fuel = let func = { id = FunOrOp (Fun (Pure FuelEqZero)); generics = empty_generic_args; } in let func_ty = mk_arrow mk_fuel_ty mk_bool_ty in let func = { e = Qualif func; ty = func_ty } in mk_app meta func fuel0 in (* Create the expression: [decrease fuel0] *) let decrease_fuel = let func = { id = FunOrOp (Fun (Pure FuelDecrease)); generics = empty_generic_args; } in let func_ty = mk_arrow mk_fuel_ty mk_fuel_ty in let func = { e = Qualif func; ty = func_ty } in mk_app meta func fuel0 in (* Create the success branch *) let monadic = false in let success_branch = mk_let monadic nfuel_pat decrease_fuel body in (* Put everything together *) let match_e = Switch (check_fuel, If (fail_branch, success_branch)) in let match_ty = body.ty in { e = match_e; ty = match_ty } | Coq -> (* Generate an expression: {[ match fuel0 with | O -> Fail OutOfFuel | S fuel -> ... }] *) (* Create the fail branch *) let fail_pat = mk_adt_pattern mk_fuel_ty (Some fuel_zero_id) [] in let fail_branch = { pat = fail_pat; branch = fail_branch } in (* Create the success branch *) let success_pat = mk_adt_pattern mk_fuel_ty (Some fuel_succ_id) [ nfuel_pat ] in let success_branch = body in let success_branch = { pat = success_pat; branch = success_branch } in (* Put everything together *) let match_ty = body.ty in let match_e = Switch (fuel0, Match [ fail_branch; success_branch ]) in { e = match_e; ty = match_ty } | Lean | HOL4 -> (* We should have checked the command line arguments before *) raise (Failure "Unexpected") let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = (* Translate *) let def = ctx.fun_decl in assert (ctx.bid = None); log#ldebug (lazy ("SymbolicToPure.translate_fun_decl: " ^ name_to_string ctx def.name ^ "\n")); (* Translate the declaration *) let def_id = def.def_id in let llbc_name = def.name in let name = name_to_string ctx llbc_name in (* Translate the signature *) let signature = translate_fun_sig_from_decomposed ctx.sg in (* Translate the body, if there is *) let body = match body with | None -> None | Some body -> let effect_info = get_fun_effect_info ctx (FunId (FRegular def_id)) None None in let body = translate_expression body ctx in (* Add a match over the fuel, if necessary *) let body = if function_decreases_fuel effect_info then wrap_in_match_fuel def.meta ctx.fuel0 ctx.fuel body else body in (* Sanity check *) type_check_texpression ctx body; (* Introduce the fuel parameter, if necessary *) let fuel = if function_uses_fuel effect_info then let fuel_var = if function_decreases_fuel effect_info then ctx.fuel0 else ctx.fuel in [ mk_fuel_var fuel_var ] else [] in (* Introduce the forward input state (the state at call site of the * *forward* function), if necessary. *) let fwd_state = (* We check if the *whole group* is stateful. See {!effect_info} *) if effect_info.stateful_group then [ mk_state_var ctx.state_var ] else [] in (* Group the inputs together *) let inputs = List.concat [ fuel; ctx.forward_inputs; fwd_state ] in let inputs_lvs = List.map (fun v -> mk_typed_pattern_from_var v None) inputs in (* Sanity check *) log#ldebug (lazy ("SymbolicToPure.translate_fun_decl: " ^ name_to_string ctx def.name ^ "\n- inputs: " ^ String.concat ", " (List.map show_var ctx.forward_inputs) ^ "\n- state: " ^ String.concat ", " (List.map show_var fwd_state) ^ "\n- signature.inputs: " ^ String.concat ", " (List.map (pure_ty_to_string ctx) signature.inputs))); (* TODO: we need to normalize the types *) if !Config.type_check_pure_code then sanity_check __FILE__ __LINE__ (List.for_all (fun (var, ty) -> (var : var).ty = ty) (List.combine inputs signature.inputs)) def.meta; Some { inputs; inputs_lvs; body } in (* Note that for now, the loops are still *inside* the function body (and we haven't counted them): we will extract them from there later, in {!PureMicroPasses} (by "splitting" the definition). *) let num_loops = 0 in let loop_id = None in (* Assemble the declaration *) let def : fun_decl = { def_id; is_local = def.is_local; meta = def.meta; kind = def.kind; num_loops; loop_id; llbc_name; name; signature; is_global_decl_body = def.is_global_decl_body; body; } in (* Debugging *) log#ldebug (lazy ("SymbolicToPure.translate_fun_decl: translated:\n" ^ fun_decl_to_string ctx def)); (* return *) def let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = List.map (translate_type_decl ctx) (TypeDeclId.Map.values ctx.type_ctx.type_decls) let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) : trait_decl = let { def_id; is_local; name = llbc_name; meta; generics = llbc_generics; preds; parent_clauses = llbc_parent_clauses; consts; types; required_methods; provided_methods; } : A.trait_decl = trait_decl in let type_infos = ctx.type_ctx.type_infos in let name = Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in let generics = translate_generic_params trait_decl.meta llbc_generics in let preds = translate_predicates trait_decl.meta preds in let parent_clauses = List.map (translate_trait_clause trait_decl.meta) llbc_parent_clauses in let consts = List.map (fun (name, (ty, id)) -> (name, (translate_fwd_ty trait_decl.meta type_infos ty, id))) consts in let types = List.map (fun (name, (trait_clauses, ty)) -> ( name, ( List.map (translate_trait_clause trait_decl.meta) trait_clauses, Option.map (translate_fwd_ty trait_decl.meta type_infos) ty ) )) types in { def_id; is_local; llbc_name; name; meta; generics; llbc_generics; preds; parent_clauses; llbc_parent_clauses; consts; types; required_methods; provided_methods; } let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) : trait_impl = let { A.def_id; is_local; name = llbc_name; meta; impl_trait = llbc_impl_trait; generics = llbc_generics; preds; parent_trait_refs; consts; types; required_methods; provided_methods; } = trait_impl in let type_infos = ctx.type_ctx.type_infos in let impl_trait = translate_trait_decl_ref trait_impl.meta (translate_fwd_ty trait_impl.meta type_infos) llbc_impl_trait in let name = Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in let generics = translate_generic_params trait_impl.meta llbc_generics in let preds = translate_predicates trait_impl.meta preds in let parent_trait_refs = List.map (translate_strait_ref trait_impl.meta) parent_trait_refs in let consts = List.map (fun (name, (ty, id)) -> (name, (translate_fwd_ty trait_impl.meta type_infos ty, id))) consts in let types = List.map (fun (name, (trait_refs, ty)) -> ( name, ( List.map (translate_fwd_trait_ref trait_impl.meta type_infos) trait_refs, translate_fwd_ty trait_impl.meta type_infos ty ) )) types in { def_id; is_local; llbc_name; name; meta; impl_trait; llbc_impl_trait; generics; llbc_generics; preds; parent_trait_refs; consts; types; required_methods; provided_methods; } let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) : global_decl = let { A.meta; def_id; is_local; name = llbc_name; generics = llbc_generics; preds; ty; kind; body = body_id; } = decl in let name = Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env ctx) llbc_name in let generics = translate_generic_params decl.meta llbc_generics in let preds = translate_predicates decl.meta preds in let ty = translate_fwd_ty decl.meta ctx.type_ctx.type_infos ty in { meta; def_id; is_local; llbc_name; name; llbc_generics; generics; preds; ty; kind; body_id; }