diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/AssociatedTypes.ml | 28 | ||||
| -rw-r--r-- | compiler/Assumed.ml | 8 | ||||
| -rw-r--r-- | compiler/Contexts.ml | 8 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 2 | ||||
| -rw-r--r-- | compiler/ExtractName.ml | 21 | ||||
| -rw-r--r-- | compiler/FunsAnalysis.ml | 55 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 12 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 31 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 10 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 796 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 12 | ||||
| -rw-r--r-- | compiler/LlbcAst.ml | 4 | ||||
| -rw-r--r-- | compiler/LlbcAstUtils.ml | 2 | ||||
| -rw-r--r-- | compiler/Main.ml | 50 | ||||
| -rw-r--r-- | compiler/Print.ml | 25 | ||||
| -rw-r--r-- | compiler/PrintPure.ml | 5 | ||||
| -rw-r--r-- | compiler/RegionsHierarchy.ml | 66 | ||||
| -rw-r--r-- | compiler/Substitute.ml | 120 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 64 | ||||
| -rw-r--r-- | compiler/Translate.ml | 2 | ||||
| -rw-r--r-- | compiler/TranslateCore.ml | 8 | ||||
| -rw-r--r-- | compiler/TypesAnalysis.ml | 2 | ||||
| -rw-r--r-- | compiler/TypesUtils.ml | 16 | ||||
| -rw-r--r-- | compiler/Values.ml | 1 |
26 files changed, 803 insertions, 551 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 2442f93a..e2f687e8 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -92,7 +92,8 @@ let ctx_add_norm_trait_types_from_preds (ctx : eval_ctx) let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool = match id with | Self | Clause _ -> true - | TraitImpl _ | BuiltinOrAuto _ | TraitRef _ | UnknownTrait _ | FnPointer _ -> + | TraitImpl _ | BuiltinOrAuto _ | TraitRef _ | UnknownTrait _ | FnPointer _ + | Closure _ -> false | ParentClause (id, _, _) | ItemClause (id, _, _, _) -> trait_instance_id_is_local_clause id @@ -118,13 +119,10 @@ let norm_ctx_to_fmt_env (ctx : norm_ctx) : Print.fmt_env = global_decls = ctx.global_decls; trait_decls = ctx.trait_decls; trait_impls = ctx.trait_impls; - generics = - { - types = ctx.type_vars; - const_generics = ctx.const_generic_vars; - regions = []; - trait_clauses = []; - }; + types = ctx.type_vars; + const_generics = ctx.const_generic_vars; + regions = []; + trait_clauses = []; preds = empty_predicates; locals = []; } @@ -220,10 +218,13 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = | TRawPtr (ty, rkind) -> let ty = norm_ctx_normalize_ty ctx ty in TRawPtr (ty, rkind) - | TArrow (inputs, output) -> + | TArrow (regions, inputs, output) -> + (* TODO: for now it works because we don't support predicates with + bound regions. If we do support them, we probably need to do + something smarter here. *) let inputs = List.map (norm_ctx_normalize_ty ctx) inputs in let output = norm_ctx_normalize_ty ctx output in - TArrow (inputs, output) + TArrow (regions, inputs, output) | TTraitType (trait_ref, generics, type_name) -> ( log#ldebug (lazy @@ -429,6 +430,9 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) (* TODO: we might want to return the ref to the function pointer, in order to later normalize a call to this function pointer *) (FnPointer ty, None) + | Closure (fid, generics) -> + let generics = norm_ctx_normalize_generic_args ctx generics in + (Closure (fid, generics), None) | UnknownTrait _ -> (* This is actually an error case *) (id, None) @@ -562,11 +566,11 @@ let ctx_adt_get_inst_norm_field_etypes (ctx : eval_ctx) (def_id : TypeDeclId.id) (** Same as [substitute_signature] but normalizes the types *) let ctx_subst_norm_signature (ctx : eval_ctx) (asubst : RegionGroupId.id -> AbstractionId.id) - (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty) + (r_subst : RegionVarId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty) (cg_subst : ConstGenericVarId.id -> const_generic) (tr_subst : TraitClauseId.id -> trait_instance_id) (tr_self : trait_instance_id) (sg : fun_sig) - (regions_hierarchy : region_groups) : inst_fun_sig = + (regions_hierarchy : region_var_groups) : inst_fun_sig = let sg = Subst.substitute_signature asubst r_subst ty_subst cg_subst tr_subst tr_self sg regions_hierarchy diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 48b7ee2b..1807add5 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -36,8 +36,8 @@ open LlbcAst module Sig = struct (** A few utilities *) - let rvar_id_0 = RegionId.of_int 0 - let rvar_0 : region = RVar rvar_id_0 + let rvar_id_0 = RegionVarId.of_int 0 + let rvar_0 : region = RBVar (0, rvar_id_0) let rg_id_0 = RegionGroupId.of_int 0 let tvar_id_0 = TypeVarId.of_int 0 let tvar_0 : ty = TVar tvar_id_0 @@ -48,7 +48,7 @@ module Sig = struct let region_param_0 : region_var = { index = rvar_id_0; name = Some "'a" } (** Region group: [{ parent={}; regions:{'a of id 0} }] *) - let region_group_0 : region_group = + let region_group_0 : region_var_group = { id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] } (** Type parameter [T] of id 0 *) @@ -84,6 +84,8 @@ module Sig = struct in { is_unsafe = false; + is_closure = false; + closure_info = None; generics; preds; parent_params_info = None; diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index c93bb213..a30ed0f1 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -190,7 +190,7 @@ type type_context = { type fun_context = { fun_decls : fun_decl FunDeclId.Map.t; fun_infos : FunsAnalysis.fun_info FunDeclId.Map.t; - regions_hierarchies : region_groups FunIdMap.t; + regions_hierarchies : region_var_groups FunIdMap.t; } [@@deriving show] @@ -241,7 +241,11 @@ type eval_ctx = { const_generic_vars_map : typed_value Types.ConstGenericVarId.Map.t; (** The map from const generic vars to their values. Those values can be symbolic values or concrete values (in the latter case: - if we run in interpreter mode) *) + if we run in interpreter mode). + + TODO: this is actually not used in symbolic mode, where we + directly introduce fresh symbolic values. + *) norm_trait_types : ty TraitTypeRefMap.t; (** The normalized trait types (a map from trait types to their representatives). Note that this doesn't take into account higher-order type constraints diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 73ccac44..43658b6e 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1984,7 +1984,7 @@ let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl) let rg = T.RegionGroupId.nth regions_hierarchy rg_id in let region_names = List.map - (fun rid -> (T.RegionId.nth sg.generics.regions rid).name) + (fun rid -> (T.RegionVarId.nth sg.generics.regions rid).name) rg.regions in Some { id = rg_id; region_names } diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml index a916bffb..4c1ffb46 100644 --- a/compiler/ExtractName.ml +++ b/compiler/ExtractName.ml @@ -3,13 +3,14 @@ open Charon.NameMatcher let log = Logging.extract_log +let match_with_trait_decl_refs = true module NameMatcherMap = struct module NMM = NameMatcherMap type 'a t = 'a NMM.t - let config = { map_vars_to_vars = true } + let config = { map_vars_to_vars = true; match_with_trait_decl_refs } let find_opt (ctx : ctx) (name : Types.name) (m : 'a t) : 'a option = NMM.find_opt ctx config name m @@ -61,7 +62,7 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) : | TArray -> "Array" | TSlice -> "Slice" else expr_to_string c ty - | ERef _ | EVar _ -> + | ERef _ | EVar _ | EArrow _ | ERawPtr _ -> (* We simply convert the pattern to a string. This is not very satisfying but we should rarely get there. *) expr_to_string c ty) @@ -85,7 +86,9 @@ let pattern_to_trait_impl_extract_name = pattern_to_extract_name true consistent with the extraction names we derive from the Rust names *) let name_to_simple_name (ctx : ctx) (is_trait_impl : bool) (n : Types.name) : string list = - let c : to_pat_config = { tgt = TkName } in + let c : to_pat_config = + { tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs } + in pattern_to_extract_name is_trait_impl (name_to_pattern ctx c n) (** If the [prefix] is Some, we attempt to remove the common prefix @@ -93,17 +96,19 @@ let name_to_simple_name (ctx : ctx) (is_trait_impl : bool) (n : Types.name) : let name_with_generics_to_simple_name (ctx : ctx) (is_trait_impl : bool) ?(prefix : Types.name option = None) (name : Types.name) (p : Types.generic_params) (g : Types.generic_args) : string list = - let c : to_pat_config = { tgt = TkName } in - let name = name_with_generics_to_pattern ctx c name p g in + let c : to_pat_config = + { tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs } + in + let name = name_with_generics_to_pattern ctx c p name g in let name = match prefix with | None -> name | Some prefix -> let prefix = - name_with_generics_to_pattern ctx c prefix - TypesUtils.empty_generic_params TypesUtils.empty_generic_args + name_with_generics_to_pattern ctx c TypesUtils.empty_generic_params + prefix TypesUtils.empty_generic_args in - let _, _, name = pattern_common_prefix prefix name in + let _, _, name = pattern_common_prefix { equiv = true } prefix name in name in pattern_to_extract_name is_trait_impl name diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 9ae6ce86..f6976f23 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -62,7 +62,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) { type_decls = m.type_decls; global_decls = m.global_decls; + fun_decls = m.fun_decls; trait_decls = m.trait_decls; + trait_impls = m.trait_impls; } in @@ -84,6 +86,16 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) method may_fail b = can_fail := !can_fail || b method maybe_stateful b = stateful := !stateful || b + method visit_fid id = + if FunDeclId.Set.mem id fun_ids then ( + can_diverge := true; + is_rec := true) + else + let info = FunDeclId.Map.find id !infos in + self#may_fail info.can_fail; + stateful := !stateful || info.stateful; + can_diverge := !can_diverge || info.can_diverge + method! visit_Assert env a = self#may_fail true; super#visit_Assert env a @@ -95,25 +107,32 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) | BinaryOp (bop, _, _) -> can_fail := binop_can_fail bop || !can_fail + method! visit_Closure env id args = + (* Remark: `Closure` is a trait instance id - TODO: rename this variant *) + self#visit_fid id; + super#visit_Closure env id args + + method! visit_AggregatedClosure env id args = + self#visit_fid id; + super#visit_AggregatedClosure env id args + method! visit_Call env call = - (match call.func.func with - | FunId (FRegular id) -> - if FunDeclId.Set.mem id fun_ids then ( - can_diverge := true; - is_rec := true) - else - let info = FunDeclId.Map.find id !infos in - self#may_fail info.can_fail; - stateful := !stateful || info.stateful; - can_diverge := !can_diverge || info.can_diverge - | FunId (FAssumed id) -> - (* None of the assumed functions can diverge nor are considered stateful *) - can_fail := !can_fail || Assumed.assumed_fun_can_fail id - | TraitMethod _ -> - (* We consider trait functions can fail, but can not diverge and are not stateful. - TODO: this may cause issues if we use use a fuel parameter. - *) - can_fail := true); + (match call.func with + | FnOpMove _ -> + (* Ignoring this: we lookup the called function upon creating + the closure *) + () + | FnOpRegular func -> ( + match func.func with + | FunId (FRegular id) -> self#visit_fid id + | FunId (FAssumed id) -> + (* None of the assumed functions can diverge nor are considered stateful *) + can_fail := !can_fail || Assumed.assumed_fun_can_fail id + | TraitMethod _ -> + (* We consider trait functions can fail, but can not diverge and are not stateful. + TODO: this may cause issues if we use use a fuel parameter. + *) + can_fail := true)); super#visit_Call env call method! visit_Panic env = diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index c2e47da9..4ecafd31 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -68,7 +68,7 @@ let normalize_inst_fun_sig (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig = normalize because a trait clause was instantiated with a specific trait ref). *) let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig) - (regions_hierarchy : region_groups) (kind : fun_kind) : + (regions_hierarchy : region_var_groups) (kind : fun_kind) : eval_ctx * inst_fun_sig = let tr_self = match kind with @@ -192,7 +192,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies in let region_groups = - List.map (fun (g : region_group) -> g.id) regions_hierarchy + List.map (fun (g : region_var_group) -> g.id) regions_hierarchy in let ctx = initialize_eval_context ctx region_groups sg.generics.types diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 2f793f4a..6a7ac095 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -448,8 +448,8 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t) | SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack -> () - | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate - | ConstGeneric | TraitConst -> + | FunCallRet | SynthInput | Global | KindConstGeneric | LoopOutput | LoopJoin + | Aggregate | ConstGeneric | TraitConst -> raise (Failure "Unreachable")); (* Store the given-back value as a meta-value for synthesis purposes *) let mv = nsv in @@ -1870,7 +1870,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) match bc with | VSharedBorrow bid -> assert (ty_no_regions ref_ty); - let ty = TRef (RVar r_id, ref_ty, kind) in + let ty = TRef (RFVar r_id, ref_ty, kind) in let value = ABorrow (ASharedBorrow bid) in ([ { value; ty } ], v) | VMutBorrow (bid, bv) -> @@ -1878,7 +1878,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) (* We don't support nested borrows for now *) assert (not (value_has_borrows ctx bv.value)); (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *) - let ty = TRef (RVar r_id, ref_ty, kind) in + let ty = TRef (RFVar r_id, ref_ty, kind) in let ignored = mk_aignored ref_ty in let av = ABorrow (AMutBorrow (bid, ignored)) in let av = { value = av; ty } in @@ -1899,7 +1899,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) (* Push the avalue - note that we use [AIgnore] for the inner avalue *) (* For avalues, a loan has the borrow type *) assert (ty_no_regions ty); - let ty = mk_ref_ty (RVar r_id) ty RShared in + let ty = mk_ref_ty (RFVar r_id) ty RShared in let ignored = mk_aignored ty in (* Rem.: the shared value might contain loans *) let avl, sv = to_avalues false true true r_id sv in @@ -1917,7 +1917,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) (* Push the avalue - note that we use [AIgnore] for the inner avalue *) (* For avalues, a loan has the borrow type *) assert (ty_no_regions ty); - let ty = mk_ref_ty (RVar r_id) ty RMut in + let ty = mk_ref_ty (RFVar r_id) ty RMut in let ignored = mk_aignored ty in let av = ALoan (AMutLoan (bid, ignored)) in let av = { value = av; ty } in diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index ac6c9ede..af545fb9 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -300,13 +300,29 @@ let eval_operand_no_reorganize (config : config) (op : operand) e )))) | CVar vid -> ( let ctx0 = ctx in - (* Lookup the const generic value *) - let cv = ctx_lookup_const_generic_value ctx vid in - (* Copy the value *) - let allow_adt_copy = false in - let ctx, v = copy_value allow_adt_copy config ctx cv in + (* In concrete mode: lookup the const generic value. + In symbolic mode: introduce a fresh symbolic value. + + We have nothing to do: the value is copyable, so we can freely + duplicate it. + *) + let ctx, cv = + let cv = ctx_lookup_const_generic_value ctx vid in + match config.mode with + | ConcreteMode -> + (* Copy the value - this is more of a sanity check *) + let allow_adt_copy = false in + copy_value allow_adt_copy config ctx cv + | SymbolicMode -> + (* We use the looked up value only for its type *) + let v = mk_fresh_symbolic_typed_value KindConstGeneric cv.ty in + (ctx, v) + in (* Continue *) - let e = cf v ctx in + let e = cf cv ctx in + (* If we are synthesizing a symbolic AST, it means that we are in symbolic + mode: the value of the const generic is necessarily symbolic. *) + assert (e = None || is_symbolic cv.value); (* We have to wrap the generated expression *) match e with | None -> None @@ -319,7 +335,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) (SymbolicAst.IntroSymbolic ( ctx0, None, - value_as_symbolic v.value, + value_as_symbolic cv.value, SymbolicAst.VaCgValue vid, e ))) | CFnPtr _ -> raise (Failure "TODO")) @@ -761,6 +777,7 @@ let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind) (* Introduce the symbolic value in the AST *) let sv = ValuesUtils.value_as_symbolic saggregated.value in Some (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e))) + | AggregatedClosure _ -> raise (Failure "Closures are not supported yet") in (* Compose and apply *) comp eval_ops compute cf diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 3cc0a5f0..c4e180fa 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -164,7 +164,7 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun = let child_av = mk_aignored child_rty in (* Create the shared loan *) - let loan_rty = TRef (RVar nrid, rty, RShared) in + let loan_rty = TRef (RFVar nrid, rty, RShared) in let loan_value = ALoan (ASharedLoan (BorrowId.Set.singleton nlid, nsv, child_av)) in diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index bf459e41..c21dab71 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -439,7 +439,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct mk_fresh_symbolic_typed_value_from_no_regions_ty LoopJoin bv_ty in - let borrow_ty = mk_ref_ty (RVar rid) bv_ty kind in + let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in (* Generate the avalues for the abstraction *) let mk_aborrow (bid : borrow_id) : typed_avalue = @@ -537,7 +537,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let kind = RMut in let bv_ty = bv.ty in assert (ty_no_regions bv_ty); - let borrow_ty = mk_ref_ty (RVar rid) bv_ty kind in + let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in let borrow_av = let ty = borrow_ty in @@ -586,7 +586,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct mk_fresh_symbolic_typed_value_from_no_regions_ty LoopJoin bv_ty in - let borrow_ty = mk_ref_ty (RVar rid) bv_ty kind in + let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in (* Generate the avalues for the abstraction *) let mk_aborrow (bid : borrow_id) (bv : typed_value) : typed_avalue = @@ -825,9 +825,9 @@ struct let match_regions r0 r1 = match (r0, r1) with | RStatic, RStatic -> r1 - | RVar rid0, RVar rid1 -> + | RFVar rid0, RFVar rid1 -> let rid = match_rid rid0 rid1 in - RVar rid + RFVar rid | _ -> raise (Distinct "match_rtys") in match_types match_distinct_types match_regions ty0 ty1 diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 9ea5387f..437b358a 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -493,77 +493,84 @@ let eval_box_free (config : config) (generics : generic_args) (** Evaluate a non-local function call in concrete mode *) let eval_assumed_function_call_concrete (config : config) (fid : assumed_fun_id) (call : call) : cm_fun = - let generics = call.func.generics in let args = call.args in let dest = call.dest in - (* Sanity check: we don't fully handle the const generic vars environment - in concrete mode yet *) - assert (generics.const_generics = []); - (* There are two cases (and this is extremely annoying): - - the function is not box_free - - the function is box_free - See {!eval_box_free} - *) - match fid with - | BoxFree -> - (* Degenerate case: box_free *) - eval_box_free config generics args dest - | _ -> - (* "Normal" case: not box_free *) - (* Evaluate the operands *) - (* let ctx, args_vl = eval_operands config ctx args in *) - let cf_eval_ops = eval_operands config args in - - (* Evaluate the call - * - * Style note: at some point we used {!comp_transmit} to - * transmit the result of {!eval_operands} above down to {!push_vars} - * below, without having to introduce an intermediary function call, - * but it made it less clear where the computed values came from, - * so we reversed the modifications. *) - let cf_eval_call cf (args_vl : typed_value list) : m_fun = - fun ctx -> - (* Push the stack frame: we initialize the frame with the return variable, - and one variable per input argument *) - let cc = push_frame in - - (* Create and push the return variable *) - let ret_vid = VarId.zero in - let ret_ty = get_assumed_function_return_type ctx fid generics in - let ret_var = mk_var ret_vid (Some "@return") ret_ty in - let cc = comp cc (push_uninitialized_var ret_var) in - - (* Create and push the input variables *) - let input_vars = - VarId.mapi_from1 - (fun id (v : typed_value) -> (mk_var id None v.ty, v)) - args_vl - in - let cc = comp cc (push_vars input_vars) in - - (* "Execute" the function body. As the functions are assumed, here we call - * custom functions to perform the proper manipulations: we don't have - * access to a body. *) - let cf_eval_body : cm_fun = - match fid with - | BoxNew -> eval_box_new_concrete config generics - | BoxFree -> - (* Should have been treated above *) raise (Failure "Unreachable") - | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared - | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut -> - raise (Failure "Unimplemented") - in + match call.func with + | FnOpMove _ -> + (* Closure case: TODO *) + raise (Failure "Closures are not supported yet") + | FnOpRegular func -> ( + let generics = func.generics in + (* Sanity check: we don't fully handle the const generic vars environment + in concrete mode yet *) + assert (generics.const_generics = []); + (* There are two cases (and this is extremely annoying): + - the function is not box_free + - the function is box_free + See {!eval_box_free} + *) + match fid with + | BoxFree -> + (* Degenerate case: box_free *) + eval_box_free config generics args dest + | _ -> + (* "Normal" case: not box_free *) + (* Evaluate the operands *) + (* let ctx, args_vl = eval_operands config ctx args in *) + let cf_eval_ops = eval_operands config args in + + (* Evaluate the call + * + * Style note: at some point we used {!comp_transmit} to + * transmit the result of {!eval_operands} above down to {!push_vars} + * below, without having to introduce an intermediary function call, + * but it made it less clear where the computed values came from, + * so we reversed the modifications. *) + let cf_eval_call cf (args_vl : typed_value list) : m_fun = + fun ctx -> + (* Push the stack frame: we initialize the frame with the return variable, + and one variable per input argument *) + let cc = push_frame in + + (* Create and push the return variable *) + let ret_vid = VarId.zero in + let ret_ty = get_assumed_function_return_type ctx fid generics in + let ret_var = mk_var ret_vid (Some "@return") ret_ty in + let cc = comp cc (push_uninitialized_var ret_var) in + + (* Create and push the input variables *) + let input_vars = + VarId.mapi_from1 + (fun id (v : typed_value) -> (mk_var id None v.ty, v)) + args_vl + in + let cc = comp cc (push_vars input_vars) in + + (* "Execute" the function body. As the functions are assumed, here we call + * custom functions to perform the proper manipulations: we don't have + * access to a body. *) + let cf_eval_body : cm_fun = + match fid with + | BoxNew -> eval_box_new_concrete config generics + | BoxFree -> + (* Should have been treated above *) + raise (Failure "Unreachable") + | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared + | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut + -> + raise (Failure "Unimplemented") + in - let cc = comp cc cf_eval_body in + let cc = comp cc cf_eval_body in - (* Pop the frame *) - let cc = comp cc (pop_frame_assign config dest) in + (* Pop the frame *) + let cc = comp cc (pop_frame_assign config dest) in - (* Continue *) - cc cf ctx - in - (* Compose and apply *) - comp cf_eval_ops cf_eval_call + (* Continue *) + cc cf ctx + in + (* Compose and apply *) + comp cf_eval_ops cf_eval_call) (** Helper @@ -652,6 +659,240 @@ let create_push_abstractions_from_abs_region_groups in List.fold_left insert_abs ctx empty_absl +(** Auxiliary helper for [eval_transparent_function_call_symbolic] + Instantiate the signature and introduce fresh abstractions and region ids while doing so. + + We perform some manipulations when instantiating the signature. + + # Trait impl calls + ================== + In particular, we have a special treatment of trait method calls when + the trait ref is a known impl. + + For instance: + {[ + trait HasValue { + fn has_value(&self) -> bool; + } + + impl<T> HasValue for Option<T> { + fn has_value(&self) { + match self { + None => false, + Some(_) => true, + } + } + } + + fn option_has_value<T>(x: &Option<T>) -> bool { + x.has_value() + } + ]} + + The generated code looks like this: + {[ + structure HasValue (Self : Type) = { + has_value : Self -> result bool + } + + let OptionHasValueImpl.has_value (Self : Type) (self : Self) : result bool = + match self with + | None => false + | Some _ => true + + let OptionHasValueInstance (T : Type) : HasValue (Option T) = { + has_value = OptionHasValueInstance.has_value + } + ]} + + In [option_has_value], we don't want to refer to the [has_value] method + of the instance of [HasValue] for [Option<T>]. We want to refer directly + to the function which implements [has_value] for [Option<T>]. + That is, instead of generating this: + {[ + let option_has_value (T : Type) (x : Option T) : result bool = + (OptionHasValueInstance T).has_value x + ]} + + We want to generate this: + {[ + let option_has_value (T : Type) (x : Option T) : result bool = + OptionHasValueImpl.has_value T x + ]} + + # Provided trait methods + ======================== + Calls to provided trait methods also have a special treatment because + for now we forbid overriding provided trait methods in the trait implementations, + which means that whenever we call a provided trait method, we do not refer + to a trait clause but directly to the method provided in the trait declaration. + *) +let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) + : fun_id_or_trait_method_ref * generic_args * fun_decl * inst_fun_sig = + match call.func with + | FnOpMove _ -> + (* Closure case: TODO *) + raise (Failure "Closures are not supported yet") + | FnOpRegular func -> ( + match func.func with + | FunId (FRegular fid) -> + let def = ctx_lookup_fun_decl ctx fid in + log#ldebug + (lazy + ("fun call:\n- call: " ^ call_to_string ctx call + ^ "\n- call.generics:\n" + ^ generic_args_to_string ctx func.generics + ^ "\n- def.signature:\n" + ^ fun_sig_to_string ctx def.signature)); + let tr_self = UnknownTrait __FUNCTION__ in + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find (FRegular fid) + ctx.fun_context.regions_hierarchies + in + let inst_sg = + instantiate_fun_sig ctx func.generics tr_self def.signature + regions_hierarchy + in + (func.func, func.generics, def, inst_sg) + | FunId (FAssumed _) -> + (* Unreachable: must be a transparent function *) + raise (Failure "Unreachable") + | TraitMethod (trait_ref, method_name, _) -> ( + log#ldebug + (lazy + ("trait method call:\n- call: " ^ call_to_string ctx call + ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n" + ^ generic_args_to_string ctx func.generics + ^ "\n- trait and method generics:\n" + ^ generic_args_to_string ctx + (Option.get func.trait_and_method_generic_args))); + (* When instantiating, we need to group the generics for the trait ref + and the method *) + let generics = Option.get func.trait_and_method_generic_args in + (* Lookup the trait method signature - there are several possibilities + depending on whethere we call a top-level trait method impl or the + method from a local clause *) + match trait_ref.trait_id with + | TraitImpl impl_id -> ( + (* Lookup the trait impl *) + let trait_impl = ctx_lookup_trait_impl ctx impl_id in + log#ldebug + (lazy ("trait impl: " ^ trait_impl_to_string ctx trait_impl)); + (* First look in the required methods *) + let method_id = + List.find_opt + (fun (s, _) -> s = method_name) + trait_impl.required_methods + in + match method_id with + | Some (_, id) -> + (* This is a required method *) + let method_def = ctx_lookup_fun_decl ctx id in + (* Instantiate *) + let tr_self = TraitRef trait_ref in + let fid : fun_id = FRegular id in + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find fid + ctx.fun_context.regions_hierarchies + in + let inst_sg = + instantiate_fun_sig ctx generics tr_self + method_def.signature regions_hierarchy + in + (* Also update the function identifier: we want to forget + the fact that we called a trait method, and treat it as + a regular function call to the top-level function + which implements the method. In order to do this properly, + we also need to update the generics. + *) + let func = FunId fid in + (func, generics, method_def, inst_sg) + | None -> + (* If not found, lookup the methods provided by the trait *declaration* + (remember: for now, we forbid overriding provided methods) *) + assert (trait_impl.provided_methods = []); + let trait_decl = + ctx_lookup_trait_decl ctx + trait_ref.trait_decl_ref.trait_decl_id + in + let _, method_id = + List.find + (fun (s, _) -> s = method_name) + trait_decl.provided_methods + in + let method_id = Option.get method_id in + let method_def = ctx_lookup_fun_decl ctx method_id in + (* For the instantiation we have to do something peculiar + because the method was defined for the trait declaration. + We have to group: + - the parameters given to the trait decl reference + - the parameters given to the method itself + For instance: + {[ + trait Foo<T> { + fn f<U>(...) { ... } + } + + fn g<G>(x : G) where Clause0: Foo<G, bool> + { + x.f::<u32>(...) // The arguments to f are: <G, bool, u32> + } + ]} + *) + let all_generics = + TypesUtils.merge_generic_args + trait_ref.trait_decl_ref.decl_generics func.generics + in + log#ldebug + (lazy + ("provided method call:" ^ "\n- method name: " + ^ method_name ^ "\n- all_generics:\n" + ^ generic_args_to_string ctx all_generics + ^ "\n- parent params info: " + ^ Print.option_to_string show_params_info + method_def.signature.parent_params_info)); + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find (FRegular method_id) + ctx.fun_context.regions_hierarchies + in + let tr_self = TraitRef trait_ref in + let inst_sg = + instantiate_fun_sig ctx all_generics tr_self + method_def.signature regions_hierarchy + in + (func.func, func.generics, method_def, inst_sg)) + | _ -> + (* We are using a local clause - we lookup the trait decl *) + let trait_decl = + ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id + in + (* Lookup the method decl in the required *and* the provided methods *) + let _, method_id = + let provided = + List.filter_map + (fun (id, f) -> + match f with None -> None | Some f -> Some (id, f)) + trait_decl.provided_methods + in + List.find + (fun (s, _) -> s = method_name) + (List.append trait_decl.required_methods provided) + in + let method_def = ctx_lookup_fun_decl ctx method_id in + log#ldebug + (lazy ("method:\n" ^ fun_decl_to_string ctx method_def)); + (* Instantiate *) + let regions_hierarchy = + LlbcAstUtils.FunIdMap.find (FRegular method_id) + ctx.fun_context.regions_hierarchies + in + let tr_self = TraitRef trait_ref in + let inst_sg = + instantiate_fun_sig ctx generics tr_self method_def.signature + regions_hierarchy + in + (func.func, func.generics, method_def, inst_sg))) + (** Evaluate a statement *) let rec eval_statement (config : config) (st : statement) : st_cm_fun = fun cf ctx -> @@ -761,7 +1002,7 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) : trait_and_method_generic_args = None; } in - let call = { func; args = []; dest } in + let call = { func = FnOpRegular func; args = []; dest } in (eval_transparent_function_call_concrete config global.body call) cf ctx | SymbolicMode -> (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be @@ -915,337 +1156,126 @@ and eval_function_call (config : config) (call : call) : st_cm_fun = and eval_function_call_concrete (config : config) (call : call) : st_cm_fun = fun cf ctx -> - match call.func.func with - | FunId (FRegular fid) -> - eval_transparent_function_call_concrete config fid call cf ctx - | FunId (FAssumed fid) -> - (* Continue - note that we do as if the function call has been successful, - * by giving {!Unit} to the continuation, because we place us in the case - * where we haven't panicked. Of course, the translation needs to take the - * panic case into account... *) - eval_assumed_function_call_concrete config fid call (cf Unit) ctx - | TraitMethod _ -> raise (Failure "Unimplemented") + match call.func with + | FnOpMove _ -> raise (Failure "Closures are not supported yet") + | FnOpRegular func -> ( + match func.func with + | FunId (FRegular fid) -> + eval_transparent_function_call_concrete config fid call cf ctx + | FunId (FAssumed fid) -> + (* Continue - note that we do as if the function call has been successful, + * by giving {!Unit} to the continuation, because we place us in the case + * where we haven't panicked. Of course, the translation needs to take the + * panic case into account... *) + eval_assumed_function_call_concrete config fid call (cf Unit) ctx + | TraitMethod _ -> raise (Failure "Unimplemented")) and eval_function_call_symbolic (config : config) (call : call) : st_cm_fun = - match call.func.func with - | FunId (FRegular _) | TraitMethod _ -> - eval_transparent_function_call_symbolic config call - | FunId (FAssumed fid) -> eval_assumed_function_call_symbolic config fid call + match call.func with + | FnOpMove _ -> raise (Failure "Closures are not supported yet") + | FnOpRegular func -> ( + match func.func with + | FunId (FRegular _) | TraitMethod _ -> + eval_transparent_function_call_symbolic config call + | FunId (FAssumed fid) -> + eval_assumed_function_call_symbolic config fid call func) (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) and eval_transparent_function_call_concrete (config : config) (fid : FunDeclId.id) (call : call) : st_cm_fun = - let generics = call.func.generics in let args = call.args in let dest = call.dest in - (* Sanity check: we don't fully handle the const generic vars environment - in concrete mode yet *) - assert (generics.const_generics = []); - fun cf ctx -> - (* Retrieve the (correctly instantiated) body *) - let def = ctx_lookup_fun_decl ctx fid in - (* We can evaluate the function call only if it is not opaque *) - let body = - match def.body with - | None -> - raise - (Failure - ("Can't evaluate a call to an opaque function: " - ^ name_to_string ctx def.name)) - | Some body -> body - in - (* TODO: we need to normalize the types if we want to correctly support traits *) - assert (generics.trait_refs = []); - (* There shouldn't be any reference to Self *) - let tr_self = UnknownTrait __FUNCTION__ in - let subst = - Subst.make_subst_from_generics def.signature.generics generics tr_self - in - let locals, body_st = Subst.fun_body_substitute_in_body subst body in - - (* Evaluate the input operands *) - assert (List.length args = body.arg_count); - let cc = eval_operands config args in - - (* Push a frame delimiter - we use {!comp_transmit} to transmit the result - * of the operands evaluation from above to the functions afterwards, while - * ignoring it in this function *) - let cc = comp_transmit cc push_frame in - - (* Compute the initial values for the local variables *) - (* 1. Push the return value *) - let ret_var, locals = - match locals with - | ret_ty :: locals -> (ret_ty, locals) - | _ -> raise (Failure "Unreachable") - in - let input_locals, locals = - Collections.List.split_at locals body.arg_count - in + match call.func with + | FnOpMove _ -> raise (Failure "Closures are not supported yet") + | FnOpRegular func -> + let generics = func.generics in + (* Sanity check: we don't fully handle the const generic vars environment + in concrete mode yet *) + assert (generics.const_generics = []); + fun cf ctx -> + (* Retrieve the (correctly instantiated) body *) + let def = ctx_lookup_fun_decl ctx fid in + (* We can evaluate the function call only if it is not opaque *) + let body = + match def.body with + | None -> + raise + (Failure + ("Can't evaluate a call to an opaque function: " + ^ name_to_string ctx def.name)) + | Some body -> body + in + (* TODO: we need to normalize the types if we want to correctly support traits *) + assert (generics.trait_refs = []); + (* There shouldn't be any reference to Self *) + let tr_self = UnknownTrait __FUNCTION__ in + let subst = + Subst.make_subst_from_generics def.signature.generics generics tr_self + in + let locals, body_st = Subst.fun_body_substitute_in_body subst body in + + (* Evaluate the input operands *) + assert (List.length args = body.arg_count); + let cc = eval_operands config args in + + (* Push a frame delimiter - we use {!comp_transmit} to transmit the result + * of the operands evaluation from above to the functions afterwards, while + * ignoring it in this function *) + let cc = comp_transmit cc push_frame in + + (* Compute the initial values for the local variables *) + (* 1. Push the return value *) + let ret_var, locals = + match locals with + | ret_ty :: locals -> (ret_ty, locals) + | _ -> raise (Failure "Unreachable") + in + let input_locals, locals = + Collections.List.split_at locals body.arg_count + in - let cc = comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty)) in + let cc = + comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty)) + in - (* 2. Push the input values *) - let cf_push_inputs cf args = - let inputs = List.combine input_locals args in - (* Note that this function checks that the variables and their values - * have the same type (this is important) *) - push_vars inputs cf - in - let cc = comp cc cf_push_inputs in - - (* 3. Push the remaining local variables (initialized as {!Bottom}) *) - let cc = comp cc (push_uninitialized_vars locals) in - - (* Execute the function body *) - let cc = comp cc (eval_function_body config body_st) in - - (* Pop the stack frame and move the return value to its destination *) - let cf_finish cf res = - match res with - | Panic -> cf Panic - | Return -> - (* Pop the stack frame, retrieve the return value, move it to - * its destination and continue *) - pop_frame_assign config dest (cf Unit) - | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ - | EndContinue _ -> - raise (Failure "Unreachable") - in - let cc = comp cc cf_finish in + (* 2. Push the input values *) + let cf_push_inputs cf args = + let inputs = List.combine input_locals args in + (* Note that this function checks that the variables and their values + * have the same type (this is important) *) + push_vars inputs cf + in + let cc = comp cc cf_push_inputs in - (* Continue *) - cc cf ctx + (* 3. Push the remaining local variables (initialized as {!Bottom}) *) + let cc = comp cc (push_uninitialized_vars locals) in + + (* Execute the function body *) + let cc = comp cc (eval_function_body config body_st) in + + (* Pop the stack frame and move the return value to its destination *) + let cf_finish cf res = + match res with + | Panic -> cf Panic + | Return -> + (* Pop the stack frame, retrieve the return value, move it to + * its destination and continue *) + pop_frame_assign config dest (cf Unit) + | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ + | EndContinue _ -> + raise (Failure "Unreachable") + in + let cc = comp cc cf_finish in + + (* Continue *) + cc cf ctx (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) and eval_transparent_function_call_symbolic (config : config) (call : call) : st_cm_fun = fun cf ctx -> - (* Instantiate the signature and introduce fresh abstractions and region ids while doing so. - - We perform some manipulations when instantiating the signature. - - # Trait impl calls - ================== - In particular, we have a special treatment of trait method calls when - the trait ref is a known impl. - - For instance: - {[ - trait HasValue { - fn has_value(&self) -> bool; - } - - impl<T> HasValue for Option<T> { - fn has_value(&self) { - match self { - None => false, - Some(_) => true, - } - } - } - - fn option_has_value<T>(x: &Option<T>) -> bool { - x.has_value() - } - ]} - - The generated code looks like this: - {[ - structure HasValue (Self : Type) = { - has_value : Self -> result bool - } - - let OptionHasValueImpl.has_value (Self : Type) (self : Self) : result bool = - match self with - | None => false - | Some _ => true - - let OptionHasValueInstance (T : Type) : HasValue (Option T) = { - has_value = OptionHasValueInstance.has_value - } - ]} - - In [option_has_value], we don't want to refer to the [has_value] method - of the instance of [HasValue] for [Option<T>]. We want to refer directly - to the function which implements [has_value] for [Option<T>]. - That is, instead of generating this: - {[ - let option_has_value (T : Type) (x : Option T) : result bool = - (OptionHasValueInstance T).has_value x - ]} - - We want to generate this: - {[ - let option_has_value (T : Type) (x : Option T) : result bool = - OptionHasValueImpl.has_value T x - ]} - - # Provided trait methods - ======================== - Calls to provided trait methods also have a special treatment because - for now we forbid overriding provided trait methods in the trait implementations, - which means that whenever we call a provided trait method, we do not refer - to a trait clause but directly to the method provided in the trait declaration. - *) let func, generics, def, inst_sg = - match call.func.func with - | FunId (FRegular fid) -> - let def = ctx_lookup_fun_decl ctx fid in - log#ldebug - (lazy - ("fun call:\n- call: " ^ call_to_string ctx call - ^ "\n- call.generics:\n" - ^ generic_args_to_string ctx call.func.generics - ^ "\n- def.signature:\n" - ^ fun_sig_to_string ctx def.signature)); - let tr_self = UnknownTrait __FUNCTION__ in - let regions_hierarchy = - LlbcAstUtils.FunIdMap.find (FRegular fid) - ctx.fun_context.regions_hierarchies - in - let inst_sg = - instantiate_fun_sig ctx call.func.generics tr_self def.signature - regions_hierarchy - in - (call.func.func, call.func.generics, def, inst_sg) - | FunId (FAssumed _) -> - (* Unreachable: must be a transparent function *) - raise (Failure "Unreachable") - | TraitMethod (trait_ref, method_name, _) -> ( - log#ldebug - (lazy - ("trait method call:\n- call: " ^ call_to_string ctx call - ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n" - ^ generic_args_to_string ctx call.func.generics - ^ "\n- trait and method generics:\n" - ^ generic_args_to_string ctx - (Option.get call.func.trait_and_method_generic_args))); - (* When instantiating, we need to group the generics for the trait ref - and the method *) - let generics = Option.get call.func.trait_and_method_generic_args in - (* Lookup the trait method signature - there are several possibilities - depending on whethere we call a top-level trait method impl or the - method from a local clause *) - match trait_ref.trait_id with - | TraitImpl impl_id -> ( - (* Lookup the trait impl *) - let trait_impl = ctx_lookup_trait_impl ctx impl_id in - log#ldebug - (lazy ("trait impl: " ^ trait_impl_to_string ctx trait_impl)); - (* First look in the required methods *) - let method_id = - List.find_opt - (fun (s, _) -> s = method_name) - trait_impl.required_methods - in - match method_id with - | Some (_, id) -> - (* This is a required method *) - let method_def = ctx_lookup_fun_decl ctx id in - (* Instantiate *) - let tr_self = TraitRef trait_ref in - let fid : fun_id = FRegular id in - let regions_hierarchy = - LlbcAstUtils.FunIdMap.find fid - ctx.fun_context.regions_hierarchies - in - let inst_sg = - instantiate_fun_sig ctx generics tr_self method_def.signature - regions_hierarchy - in - (* Also update the function identifier: we want to forget - the fact that we called a trait method, and treat it as - a regular function call to the top-level function - which implements the method. In order to do this properly, - we also need to update the generics. - *) - let func = FunId fid in - (func, generics, method_def, inst_sg) - | None -> - (* If not found, lookup the methods provided by the trait *declaration* - (remember: for now, we forbid overriding provided methods) *) - assert (trait_impl.provided_methods = []); - let trait_decl = - ctx_lookup_trait_decl ctx - trait_ref.trait_decl_ref.trait_decl_id - in - let _, method_id = - List.find - (fun (s, _) -> s = method_name) - trait_decl.provided_methods - in - let method_id = Option.get method_id in - let method_def = ctx_lookup_fun_decl ctx method_id in - (* For the instantiation we have to do something peculiar - because the method was defined for the trait declaration. - We have to group: - - the parameters given to the trait decl reference - - the parameters given to the method itself - For instance: - {[ - trait Foo<T> { - fn f<U>(...) { ... } - } - - fn g<G>(x : G) where Clause0: Foo<G, bool> - { - x.f::<u32>(...) // The arguments to f are: <G, bool, u32> - } - ]} - *) - let all_generics = - TypesUtils.merge_generic_args - trait_ref.trait_decl_ref.decl_generics call.func.generics - in - log#ldebug - (lazy - ("provided method call:" ^ "\n- method name: " ^ method_name - ^ "\n- all_generics:\n" - ^ generic_args_to_string ctx all_generics - ^ "\n- parent params info: " - ^ Print.option_to_string show_params_info - method_def.signature.parent_params_info)); - let regions_hierarchy = - LlbcAstUtils.FunIdMap.find (FRegular method_id) - ctx.fun_context.regions_hierarchies - in - let tr_self = TraitRef trait_ref in - let inst_sg = - instantiate_fun_sig ctx all_generics tr_self - method_def.signature regions_hierarchy - in - (call.func.func, call.func.generics, method_def, inst_sg)) - | _ -> - (* We are using a local clause - we lookup the trait decl *) - let trait_decl = - ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id - in - (* Lookup the method decl in the required *and* the provided methods *) - let _, method_id = - let provided = - List.filter_map - (fun (id, f) -> - match f with None -> None | Some f -> Some (id, f)) - trait_decl.provided_methods - in - List.find - (fun (s, _) -> s = method_name) - (List.append trait_decl.required_methods provided) - in - let method_def = ctx_lookup_fun_decl ctx method_id in - log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def)); - (* Instantiate *) - let regions_hierarchy = - LlbcAstUtils.FunIdMap.find (FRegular method_id) - ctx.fun_context.regions_hierarchies - in - let tr_self = TraitRef trait_ref in - let inst_sg = - instantiate_fun_sig ctx generics tr_self method_def.signature - regions_hierarchy - in - (call.func.func, call.func.generics, method_def, inst_sg)) + eval_transparent_function_call_symbolic_inst call ctx in (* Sanity check *) assert (List.length call.args = List.length def.signature.inputs); @@ -1408,9 +1438,9 @@ and eval_function_call_symbolic_from_inst_sig (config : config) (** Evaluate a non-local function call in symbolic mode *) and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) - (call : call) : st_cm_fun = + (call : call) (func : fn_ptr) : st_cm_fun = fun cf ctx -> - let generics = call.func.generics in + let generics = func.generics in let args = call.args in let dest = call.dest in (* Sanity check: make sure the type parameters don't contain regions - diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index bba88e9f..d3f8f4fa 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -273,8 +273,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : eval_ctx) raise Found else () | SynthInput | SynthInputGivenBack | FunCallGivenBack - | SynthRetGivenBack | Global | LoopGivenBack | Aggregate | ConstGeneric - | TraitConst -> + | SynthRetGivenBack | Global | KindConstGeneric | LoopGivenBack + | Aggregate | ConstGeneric | TraitConst -> () end in @@ -455,7 +455,7 @@ let initialize_eval_context (ctx : decls_ctx) *) let instantiate_fun_sig (ctx : eval_ctx) (generics : generic_args) (tr_self : trait_instance_id) (sg : fun_sig) - (regions_hierarchy : region_groups) : inst_fun_sig = + (regions_hierarchy : region_var_groups) : inst_fun_sig = log#ldebug (lazy ("instantiate_fun_sig:" ^ "\n- generics: " @@ -484,7 +484,11 @@ let instantiate_fun_sig (ctx : eval_ctx) (generics : generic_args) RegionGroupId.Map.find rg_id asubst_map in (* Generate fresh regions and their substitutions *) - let _, rsubst, _ = Substitute.fresh_regions_with_substs sg.generics.regions in + let _, rsubst, _ = + Substitute.fresh_regions_with_substs_from_vars ~fail_if_not_found:true + sg.generics.regions + in + let rsubst r = Option.get (rsubst r) in (* Generate the type substitution Note that for now we don't support instantiating the type parameters with types containing regions. *) diff --git a/compiler/LlbcAst.ml b/compiler/LlbcAst.ml index 9772671e..e071b36f 100644 --- a/compiler/LlbcAst.ml +++ b/compiler/LlbcAst.ml @@ -2,7 +2,9 @@ open Types open Values include Charon.LlbcAst -type abs_region_group = AbstractionId.id g_region_group [@@deriving show] +type abs_region_group = (RegionId.id, AbstractionId.id) g_region_group +[@@deriving show] + type abs_region_groups = abs_region_group list [@@deriving show] (** A function signature, after instantiation *) diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index ffdce481..d3fac032 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -35,7 +35,9 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : { type_decls = k.type_decls; global_decls = k.global_decls; + fun_decls = k.fun_decls; trait_decls = k.trait_decls; + trait_impls = k.trait_impls; } in let is_opaque_fun (d : fun_decl) : bool = diff --git a/compiler/Main.ml b/compiler/Main.ml index 7f98f581..835b9088 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -66,7 +66,7 @@ let () = (* Print the imported llbc *) let print_llbc = ref false in - let spec = + let spec_ls = [ ( "-backend", Arg.Symbol (backend_names, set_backend), @@ -123,7 +123,7 @@ let () = ] in - let spec = Arg.align spec in + let spec = Arg.align spec_ls in let filenames = ref [] in let add_filename f = filenames := f :: !filenames in Arg.parse spec add_filename usage; @@ -132,20 +132,50 @@ let () = exit 1 in - if !extract_template_decreases_clauses then extract_decreases_clauses := true; + (* Small helper to check the validity of the input arguments and print + an error if necessary *) + let check_arg_name name = + assert (List.exists (fun (n, _, _) -> n = name) spec_ls) + in + let check_arg_implies (arg0 : bool) (name0 : string) (arg1 : bool) + (name1 : string) : unit = + check_arg_name name0; + check_arg_name name1; + if (not arg0) || arg1 then () + else ( + log#error "Invalid command-line arguments: the use of %s requires %s" + name0 name1; + fail ()) + in + + let check_arg_not (arg0 : bool) (name0 : string) (arg1 : bool) + (name1 : string) : unit = + check_arg_name name0; + check_arg_name name1; + if (not arg0) || not arg1 then () + else ( + log#error + "Invalid command-line arguments: the use of %s is incompatible with %s" + name0 name1; + fail ()) + in + if !print_llbc then main_log#set_level EL.Debug; (* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *) - assert (!extract_decreases_clauses || not !extract_template_decreases_clauses); + check_arg_implies + !extract_template_decreases_clauses + "-template-clauses" !extract_decreases_clauses "-decreases-clauses"; (* Sanity check: -backward-no-state-update ==> -state *) - assert ((not !backward_no_state_update) || !use_state); + check_arg_implies !backward_no_state_update "-backward-no-state-update" + !use_state "-state"; (* Sanity check: the use of decrease clauses is not compatible with the use of fuel *) - assert ( - (not !use_fuel) - || (not !extract_decreases_clauses) - && not !extract_template_decreases_clauses); + check_arg_not !use_fuel "-use-fuel" !extract_decreases_clauses + "-decreases-clauses"; (* We have: not generate_lib_entry_point ==> split_files *) - assert (!split_files || !generate_lib_entry_point); + check_arg_implies + (not !generate_lib_entry_point) + "-no-gen-lib-entry" !split_files "-split-files"; if !lean_gen_lakefile && not (!backend = Lean) then log#error "The -lean-default-lakefile option is valid only for the Lean backend"; diff --git a/compiler/Print.ml b/compiler/Print.ml index 92ce6f23..0e2ec1fc 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -393,7 +393,6 @@ module Contexts = struct let global_decls = ctx.global_ctx.global_decls in let trait_decls = ctx.trait_decls_ctx.trait_decls in let trait_impls = ctx.trait_impls_ctx.trait_impls in - let generics = TypesUtils.empty_generic_params in let preds = TypesUtils.empty_predicates in { type_decls; @@ -401,7 +400,10 @@ module Contexts = struct global_decls; trait_decls; trait_impls; - generics; + regions = []; + types = []; + const_generics = []; + trait_clauses = []; preds; locals = []; } @@ -415,16 +417,6 @@ module Contexts = struct (* Below: it is always safe to omit fields - if an id can't be found at printing time, we print the id (in raw form) instead of the name it designates. *) - let generics : generic_params = - { - types = ctx.type_vars; - (* The regions have been transformed to region groups *) - regions = []; - const_generics = ctx.const_generic_vars; - (* We don't need the trait clauses so we initialize them to empty *) - trait_clauses = []; - } - in (* We don't need the predicates so we initialize them to empty *) let preds = empty_predicates in (* For the locals: we retrieve the information from the environment. @@ -444,7 +436,12 @@ module Contexts = struct global_decls; trait_decls; trait_impls; - generics; + types = ctx.type_vars; + (* The regions have been transformed to region groups *) + regions = []; + const_generics = ctx.const_generic_vars; + (* We don't need the trait clauses so we initialize them to empty *) + trait_clauses = []; preds; locals; } @@ -596,7 +593,7 @@ module EvalCtx = struct let fun_id_or_trait_method_ref_to_string (ctx : eval_ctx) (x : fun_id_or_trait_method_ref) : string = let env = eval_ctx_to_fmt_env ctx in - fun_id_or_trait_method_ref_to_string env x "..." + fun_id_or_trait_method_ref_to_string env x let statement_to_string (ctx : eval_ctx) (indent : string) (indent_incr : string) (e : statement) : string = diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 5d8297d3..d33a2f18 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -56,7 +56,10 @@ let fmt_env_to_llbc_fmt_env (env : fmt_env) : Print.fmt_env = global_decls = env.global_decls; trait_decls = env.trait_decls; trait_impls = env.trait_impls; - generics = TypesUtils.empty_generic_params; + regions = []; + types = []; + const_generics = []; + trait_clauses = []; preds = TypesUtils.empty_predicates; locals = []; } diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index e101ba49..80b67a54 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -23,6 +23,8 @@ have to compute the SCCs of the lifetimes (two lifetimes 'a and 'b may satisfy 'a : 'b and 'b : 'a, meaning they are actually equal and should be grouped together). + + TODO: we don't handle locally bound regions yet. *) open Types @@ -42,7 +44,7 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) (global_decls : global_decl GlobalDeclId.Map.t) (trait_decls : trait_decl TraitDeclId.Map.t) (trait_impls : trait_impl TraitImplId.Map.t) (fun_name : string) - (sg : fun_sig) : region_groups = + (sg : fun_sig) : region_var_groups = log#ldebug (lazy (__FUNCTION__ ^ ": " ^ fun_name)); (* Initialize a normalization context (we may need to normalize some associated types) *) @@ -74,12 +76,27 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) - the region variables - the static region - edges from the region variables to the static region + + Note that we introduce free variables for all the regions bound at the + level of the signature (this excludes the regions locally bound inside + the types, for instance at the level of an arrow type). *) + let bound_regions, bound_regions_id_subst, bound_regions_subst = + Subst.fresh_regions_with_substs_from_vars ~fail_if_not_found:true + sg.generics.regions + in + let region_id_to_var_map : RegionVarId.id RegionId.Map.t = + RegionId.Map.of_list + (List.combine bound_regions + (List.map (fun (r : region_var) -> r.index) sg.generics.regions)) + in + let subst = { Subst.empty_subst with r_subst = bound_regions_subst } in let g : RegionSet.t RegionMap.t ref = let s_set = RegionSet.singleton RStatic in let m = List.map - (fun (r : region_var) -> (RVar r.index, s_set)) + (fun (r : region_var) -> + (RFVar (Option.get (bound_regions_id_subst r.index)), s_set)) sg.generics.regions in let s = (RStatic, RegionSet.empty) in @@ -87,10 +104,17 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) in let add_edge ~(short : region) ~(long : region) = - let m = !g in - let s = RegionMap.find short !g in - let s = RegionSet.add long s in - g := RegionMap.add short s m + (* Sanity checks *) + assert (short <> RErased); + assert (long <> RErased); + (* Ignore the locally bound regions (at the level of arrow types for instance *) + match (short, long) with + | RBVar _, _ | _, RBVar _ -> () + | _, _ -> + let m = !g in + let s = RegionMap.find short !g in + let s = RegionSet.add long s in + g := RegionMap.add short s m in let add_edge_from_region_constraint ((long, short) : region_outlives) = @@ -152,22 +176,30 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id); (* We have nothing to do *) () - | TArrow (inputs, output) -> - (* TODO: this may be too constraining *) - List.iter (explore_ty outer) (output :: inputs) + | TArrow (regions, inputs, output) -> + (* TODO: *) + assert (regions = []); + (* We can ignore the outer regions *) + List.iter (explore_ty []) (output :: inputs) and explore_generics (outer : region list) (generics : generic_args) = let { regions; types; const_generics = _; trait_refs = _ } = generics in List.iter (fun long -> add_edges ~long ~shorts:outer) regions; List.iter (explore_ty outer) types in + (* Substitute the regions in a type, then explore *) + let explore_ty_subst ty = + let ty = Subst.ty_substitute subst ty in + explore_ty [] ty + in + (* Normalize the types then explore *) let tys = List.map (AssociatedTypes.norm_ctx_normalize_ty norm_ctx) (sg.output :: sg.inputs) in - List.iter (explore_ty []) tys; + List.iter explore_ty_subst tys; (* Compute the ordered SCCs *) let module Scc = SCC.Make (RegionOrderedType) in @@ -240,10 +272,12 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) let id = RegionGroupId.of_int i in (* Retrieve the set of regions in the group *) - let regions = + let regions : RegionVarId.id list = List.map (fun r -> - match r with RVar r -> r | _ -> raise (Failure "Unreachable")) + match r with + | RFVar rid -> RegionId.Map.find rid region_id_to_var_map + | _ -> raise (Failure "Unreachable")) scc in @@ -262,7 +296,8 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t) (fun_decls : fun_decl FunDeclId.Map.t) (global_decls : global_decl GlobalDeclId.Map.t) (trait_decls : trait_decl TraitDeclId.Map.t) - (trait_impls : trait_impl TraitImplId.Map.t) : region_groups FunIdMap.t = + (trait_impls : trait_impl TraitImplId.Map.t) : region_var_groups FunIdMap.t + = let open Print in let env : fmt_env = { @@ -271,7 +306,10 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t) global_decls; trait_decls; trait_impls; - generics = empty_generic_params; + regions = []; + types = []; + const_generics = []; + trait_clauses = []; preds = empty_predicates; locals = []; } diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index a05b2c5a..e28f005d 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -11,6 +11,9 @@ open Contexts type subst = { r_subst : region -> region; + (** Remark: this might be called with bound regions with a negative + DeBruijn index. A negative DeBruijn index means that the region + is locally bound. *) ty_subst : TypeVarId.id -> ty; cg_subst : ConstGenericVarId.id -> const_generic; (** Substitution from *local* trait clause to trait instance *) @@ -19,11 +22,35 @@ type subst = { tr_self : trait_instance_id; } +let empty_subst : subst = + { + r_subst = (fun x -> x); + ty_subst = (fun id -> TVar id); + cg_subst = (fun id -> CgVar id); + tr_subst = (fun id -> Clause id); + tr_self = Self; + } + let st_substitute_visitor (subst : subst) = - object + object (self) inherit [_] map_statement - method! visit_region _ r = subst.r_subst r - method! visit_TVar _ id = subst.ty_subst id + method! visit_region (subst : subst) r = subst.r_subst r + + (** We need to properly handle the DeBruijn indices *) + method! visit_TArrow subst regions inputs output = + (* Decrement the DeBruijn indices before calling the substitution *) + let r_subst r = + match r with + | RBVar (db, rid) -> subst.r_subst (RBVar (db - 1, rid)) + | _ -> subst.r_subst r + in + let subst = { subst with r_subst } in + (* Note that we ignore the bound regions variables *) + let inputs = List.map (self#visit_ty subst) inputs in + let output = self#visit_ty subst output in + TArrow (regions, inputs, output) + + method! visit_TVar (subst : subst) id = subst.ty_subst id method! visit_type_var_id _ _ = (* We should never get here because we reimplemented [visit_TypeVar] *) @@ -35,8 +62,8 @@ let st_substitute_visitor (subst : subst) = (* We should never get here because we reimplemented [visit_Var] *) raise (Failure "Unexpected") - method! visit_Clause _ id = subst.tr_subst id - method! visit_Self _ = subst.tr_self + method! visit_Clause (subst : subst) id = subst.tr_subst id + method! visit_Self (subst : subst) = subst.tr_self end (** Substitute types variables and regions in a type. @@ -45,27 +72,27 @@ let st_substitute_visitor (subst : subst) = *) let ty_substitute (subst : subst) (ty : ty) : ty = let visitor = st_substitute_visitor subst in - visitor#visit_ty () ty + visitor#visit_ty subst ty (** **IMPORTANT**: this doesn't normalize the types. *) let trait_ref_substitute (subst : subst) (tr : trait_ref) : trait_ref = let visitor = st_substitute_visitor subst in - visitor#visit_trait_ref () tr + visitor#visit_trait_ref subst tr (** **IMPORTANT**: this doesn't normalize the types. *) let trait_instance_id_substitute (subst : subst) (tr : trait_instance_id) : trait_instance_id = let visitor = st_substitute_visitor subst in - visitor#visit_trait_instance_id () tr + visitor#visit_trait_instance_id subst tr (** **IMPORTANT**: this doesn't normalize the types. *) let generic_args_substitute (subst : subst) (g : generic_args) : generic_args = let visitor = st_substitute_visitor subst in - visitor#visit_generic_args () g + visitor#visit_generic_args subst g let predicates_substitute (subst : subst) (p : predicates) : predicates = let visitor = st_substitute_visitor subst in - visitor#visit_predicates () p + visitor#visit_predicates subst p let erase_regions_subst : subst = { @@ -96,26 +123,40 @@ let generic_args_erase_regions (tr : generic_args) : generic_args = TODO: simplify? we only need the subst [RegionVarId.id -> RegionId.id] *) -let fresh_regions_with_substs (region_vars : region_var list) : - RegionId.id list * (RegionId.id -> RegionId.id) * (region -> region) = +let fresh_regions_with_substs ~(fail_if_not_found : bool) + (region_vars : RegionVarId.id list) : + RegionId.id list + * (RegionVarId.id -> RegionId.id option) + * (region -> region) = (* Generate fresh regions *) let fresh_region_ids = List.map (fun _ -> fresh_region_id ()) region_vars in (* Generate the map from region var ids to regions *) let ls = List.combine region_vars fresh_region_ids in - let rid_map = - List.fold_left - (fun mp ((k : region_var), v) -> RegionId.Map.add k.index v mp) - RegionId.Map.empty ls - in + let rid_map = RegionVarId.Map.of_list ls in (* Generate the substitution from region var id to region *) - let rid_subst id = RegionId.Map.find id rid_map in + let rid_subst id = RegionVarId.Map.find_opt id rid_map in (* Generate the substitution from region to region *) let r_subst (r : region) = - match r with RStatic | RErased -> r | RVar id -> RVar (rid_subst id) + match r with + | RStatic | RErased | RFVar _ -> r + | RBVar (bdid, id) -> + if bdid = 0 then + match rid_subst id with + | None -> if fail_if_not_found then raise Not_found else r + | Some r -> RFVar r + else r in (* Return *) (fresh_region_ids, rid_subst, r_subst) +let fresh_regions_with_substs_from_vars ~(fail_if_not_found : bool) + (region_vars : region_var list) : + RegionId.id list + * (RegionVarId.id -> RegionId.id option) + * (region -> region) = + fresh_regions_with_substs ~fail_if_not_found + (List.map (fun (r : region_var) -> r.index) region_vars) + (** Erase the regions in a type and perform a substitution *) let erase_regions_substitute_types (ty_subst : TypeVarId.id -> ty) (cg_subst : ConstGenericVarId.id -> const_generic) @@ -127,16 +168,21 @@ let erase_regions_substitute_types (ty_subst : TypeVarId.id -> ty) (** Create a region substitution from a list of region variable ids and a list of regions (with which to substitute the region variable ids *) -let make_region_subst (var_ids : RegionId.id list) (regions : region list) : +let make_region_subst (var_ids : RegionVarId.id list) (regions : region list) : region -> region = let ls = List.combine var_ids regions in let mp = List.fold_left - (fun mp (k, v) -> RegionId.Map.add k v mp) - RegionId.Map.empty ls + (fun mp (k, v) -> RegionVarId.Map.add k v mp) + RegionVarId.Map.empty ls in fun r -> - match r with RStatic | RErased -> r | RVar id -> RegionId.Map.find id mp + match r with + | RStatic | RErased -> r + | RFVar _ -> raise (Failure "Unexpected") + | RBVar (bdid, id) -> + (* Only substitute the bound regions with DeBruijn index equal to 0 *) + if bdid = 0 then RegionVarId.Map.find id mp else r let make_region_subst_from_vars (vars : region_var list) (regions : region list) : region -> region = @@ -298,27 +344,27 @@ let ctx_adt_value_get_instantiated_field_types (ctx : eval_ctx) (** Apply a type substitution to a place *) let place_substitute (subst : subst) (p : place) : place = (* There is in fact nothing to do *) - (st_substitute_visitor subst)#visit_place () p + (st_substitute_visitor subst)#visit_place subst p (** Apply a type substitution to an operand *) let operand_substitute (subst : subst) (op : operand) : operand = - (st_substitute_visitor subst)#visit_operand () op + (st_substitute_visitor subst)#visit_operand subst op (** Apply a type substitution to an rvalue *) let rvalue_substitute (subst : subst) (rv : rvalue) : rvalue = - (st_substitute_visitor subst)#visit_rvalue () rv + (st_substitute_visitor subst)#visit_rvalue subst rv (** Apply a type substitution to an assertion *) let assertion_substitute (subst : subst) (a : assertion) : assertion = - (st_substitute_visitor subst)#visit_assertion () a + (st_substitute_visitor subst)#visit_assertion subst a (** Apply a type substitution to a call *) let call_substitute (subst : subst) (call : call) : call = - (st_substitute_visitor subst)#visit_call () call + (st_substitute_visitor subst)#visit_call subst call (** Apply a type substitution to a statement *) let statement_substitute (subst : subst) (st : statement) : statement = - (st_substitute_visitor subst)#visit_statement () st + (st_substitute_visitor subst)#visit_statement subst st (** Apply a type substitution to a function body. Return the local variables and the body. *) @@ -336,9 +382,9 @@ let trait_type_constraint_substitute (subst : subst) (ttc : trait_type_constraint) : trait_type_constraint = let { trait_ref; generics; type_name; ty } = ttc in let visitor = st_substitute_visitor subst in - let trait_ref = visitor#visit_trait_ref () trait_ref in - let generics = visitor#visit_generic_args () generics in - let ty = visitor#visit_ty () ty in + let trait_ref = visitor#visit_trait_ref subst trait_ref in + let generics = visitor#visit_generic_args subst generics in + let ty = visitor#visit_ty subst ty in { trait_ref; generics; type_name; ty } (** Substitute a function signature, together with the regions hierarchy @@ -347,18 +393,20 @@ let trait_type_constraint_substitute (subst : subst) **IMPORTANT:** this function doesn't normalize the types. *) let substitute_signature (asubst : RegionGroupId.id -> AbstractionId.id) - (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty) + (r_subst : RegionVarId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty) (cg_subst : ConstGenericVarId.id -> const_generic) (tr_subst : TraitClauseId.id -> trait_instance_id) (tr_self : trait_instance_id) (sg : fun_sig) - (regions_hierarchy : region_groups) : inst_fun_sig = + (regions_hierarchy : region_var_groups) : inst_fun_sig = let r_subst' (r : region) : region = - match r with RStatic | RErased -> r | RVar rid -> RVar (r_subst rid) + match r with + | RStatic | RErased | RFVar _ -> r + | RBVar (bdid, rid) -> if bdid = 0 then RFVar (r_subst rid) else r in let subst = { r_subst = r_subst'; ty_subst; cg_subst; tr_subst; tr_self } in let inputs = List.map (ty_substitute subst) sg.inputs in let output = ty_substitute subst sg.output in - let subst_region_group (rg : region_group) : abs_region_group = + let subst_region_group (rg : region_var_group) : abs_region_group = let id = asubst rg.id in let regions = List.map r_subst rg.regions in let parents = List.map asubst rg.parents in diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index f5b055fd..3b30549c 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -47,7 +47,7 @@ type fun_context = { llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t; fun_sigs : fun_sig_named_outputs RegularFunIdNotLoopMap.t; (** *) fun_infos : fun_info A.FunDeclId.Map.t; - regions_hierarchies : T.region_groups FunIdMap.t; + regions_hierarchies : T.region_var_groups FunIdMap.t; } [@@deriving show] @@ -214,7 +214,9 @@ let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env = let global_decls = ctx.global_context.llbc_global_decls in let trait_decls = ctx.trait_decls_ctx in let trait_impls = ctx.trait_impls_ctx in - let generics = ctx.fun_decl.signature.generics 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; @@ -222,7 +224,10 @@ let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env = global_decls; trait_decls; trait_impls; - generics; + regions = [ regions ]; + types; + const_generics; + trait_clauses; preds; locals = []; } @@ -279,6 +284,10 @@ let texpression_to_string (ctx : bs_ctx) (e : texpression) : string = let env = bs_ctx_to_pure_fmt_env ctx in PrintPure.texpression_to_string 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 @@ -371,7 +380,7 @@ and translate_trait_instance_id (translate_ty : T.ty -> ty) 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 translate_ty tr) - | FnPointer _ -> raise (Failure "TODO") + | FnPointer _ | Closure _ -> raise (Failure "Closures are not supported yet") | UnknownTrait s -> raise (Failure ("Unknown trait found: " ^ s)) (** Translate a signature type - TODO: factor out the different translation functions *) @@ -873,7 +882,7 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id) (* Create the context *) let ctx = let region_groups = - List.map (fun (g : T.region_group) -> g.id) regions_hierarchy + List.map (fun (g : T.region_var_group) -> g.id) regions_hierarchy in let ctx = InterpreterUtils.initialize_eval_context decls_ctx region_groups @@ -905,17 +914,30 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id) * so just check that there aren't parent regions *) assert (T.RegionGroupId.Set.is_empty parents); (* Small helper to translate types for backward functions *) - let translate_back_ty_for_gid (gid : T.RegionGroupId.id) : T.ty -> ty option = + let translate_back_ty_for_gid (gid : T.RegionGroupId.id) (ty : T.ty) : + ty option = let rg = T.RegionGroupId.nth regions_hierarchy gid in - let regions = T.RegionId.Set.of_list rg.regions 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 - | T.RErased -> raise (Failure "Unexpected erased region") - | T.RVar r -> T.RegionId.Set.mem r regions + | RErased -> raise (Failure "Unexpected erased region") + | RBVar _ -> raise (Failure "Unexpected bound region") + | RFVar rid -> T.RegionId.Set.mem rid gr_regions in let inside_mut = false in - translate_back_ty type_infos keep_region inside_mut + translate_back_ty type_infos keep_region inside_mut ty in (* Compute the additinal inputs for the current function, if it is a backward * function *) @@ -1064,6 +1086,8 @@ let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern = (* Return *) (ctx, 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 *) @@ -1749,7 +1773,8 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : is_rec = false; } in - (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, None)) + (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, None) + | CastFnPtr _ -> raise (Failure "TODO: function casts")) | S.Binop binop -> ( match args with | [ arg0; arg1 ] -> @@ -1758,8 +1783,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : (match binop with (* The Rust compiler accepts bitshifts for any integer type combination for ty0, ty1 *) | E.Shl | E.Shr -> () - | _ -> assert (int_ty0 = int_ty1) - ); + | _ -> assert (int_ty0 = int_ty1)); let effect_info = { can_fail = ExpressionsUtils.binop_can_fail binop; @@ -2484,9 +2508,13 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_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 *) + (* Introduce a fresh variable for the symbolic value. *) let ctx, var = fresh_var_for_symbolic_value sv ctx in (* Translate the next expression *) @@ -3100,6 +3128,12 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx) let translate_one (fun_id : A.fun_id) (input_names : string option list) (sg : A.fun_sig) : (regular_fun_id_not_loop * fun_sig_named_outputs) list = + log#ldebug + (lazy + ("Translating signature of function: " + ^ Print.Expressions.fun_id_to_string + (Print.Contexts.decls_ctx_to_fmt_env decls_ctx) + fun_id)); (* Retrieve the regions hierarchy *) let regions_hierarchy = FunIdMap.find fun_id decls_ctx.fun_ctx.regions_hierarchies @@ -3110,7 +3144,7 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx) (* The backward functions *) let back_sgs = List.map - (fun (rg : T.region_group) -> + (fun (rg : T.region_var_group) -> let tsg = translate_fun_sig decls_ctx fun_id sg input_names (Some rg.id) in diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 37f58140..221d4e73 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -188,7 +188,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) in (* Translate the backward functions *) - let translate_backward (rg : region_group) : Pure.fun_decl = + let translate_backward (rg : region_var_group) : Pure.fun_decl = (* For the backward inputs/outputs initialization: we use the fact that * there are no nested borrows for now, and so that the region groups * can't have parents *) diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml index abf4fcf7..88438872 100644 --- a/compiler/TranslateCore.ml +++ b/compiler/TranslateCore.ml @@ -39,7 +39,9 @@ let match_name_find_opt (ctx : trans_ctx) (name : Types.name) { type_decls = ctx.type_ctx.type_decls; global_decls = ctx.global_ctx.global_decls; + fun_decls = ctx.fun_ctx.fun_decls; trait_decls = ctx.trait_decls_ctx.trait_decls; + trait_impls = ctx.trait_impls_ctx.trait_impls; } in NameMatcherMap.find_opt mctx name m @@ -52,7 +54,9 @@ let match_name_with_generics_find_opt (ctx : trans_ctx) (name : Types.name) { type_decls = ctx.type_ctx.type_decls; global_decls = ctx.global_ctx.global_decls; + fun_decls = ctx.fun_ctx.fun_decls; trait_decls = ctx.trait_decls_ctx.trait_decls; + trait_impls = ctx.trait_impls_ctx.trait_impls; } in NameMatcherMap.find_with_generics_opt mctx name generics m @@ -62,7 +66,9 @@ let name_to_simple_name (ctx : trans_ctx) (n : Types.name) : string list = { type_decls = ctx.type_ctx.type_decls; global_decls = ctx.global_ctx.global_decls; + fun_decls = ctx.fun_ctx.fun_decls; trait_decls = ctx.trait_decls_ctx.trait_decls; + trait_impls = ctx.trait_impls_ctx.trait_impls; } in let is_trait_impl = false in @@ -75,7 +81,9 @@ let trait_name_with_generics_to_simple_name (ctx : trans_ctx) { type_decls = ctx.type_ctx.type_decls; global_decls = ctx.global_ctx.global_decls; + fun_decls = ctx.fun_ctx.fun_decls; trait_decls = ctx.trait_decls_ctx.trait_decls; + trait_impls = ctx.trait_impls_ctx.trait_impls; } in let is_trait_impl = true in diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml index eb0aeea9..589c380c 100644 --- a/compiler/TypesAnalysis.ml +++ b/compiler/TypesAnalysis.ml @@ -233,7 +233,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos) in (* Return *) ty_info - | TArrow (inputs, output) -> + | TArrow (_regions, inputs, output) -> (* Just dive into the arrow *) let ty_info = List.fold_left diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml index 76cc710a..c8418ba0 100644 --- a/compiler/TypesUtils.ml +++ b/compiler/TypesUtils.ml @@ -29,16 +29,19 @@ let ty_has_borrow_under_mut (infos : TypesAnalysis.type_infos) (ty : ty) : bool info.TypesAnalysis.contains_borrow_under_mut (** Small helper *) -let raise_if_erased_ty_visitor = +let raise_if_not_rty_visitor = object inherit [_] iter_ty - method! visit_RErased _ = raise Found + + method! visit_region _ r = + match r with RBVar _ | RErased -> raise Found | RStatic | RFVar _ -> () end -(** Return [true] if the type is a region type (i.e., it doesn't contain erased regions) *) +(** Return [true] if the type is a region type (i.e., it doesn't contain erased + regions), and only contains free regions) *) let ty_is_rty (ty : ty) : bool = try - raise_if_erased_ty_visitor#visit_ty () ty; + raise_if_not_rty_visitor#visit_ty () ty; true with Found -> false @@ -46,8 +49,9 @@ let ty_is_rty (ty : ty) : bool = let raise_if_not_erased_ty_visitor = object inherit [_] iter_ty - method! visit_RStatic _ = raise Found - method! visit_RVar _ = raise Found + + method! visit_region _ r = + match r with RStatic | RBVar _ | RFVar _ -> raise Found | RErased -> () end (** Return [true] if the type is a region type (i.e., it doesn't contain erased regions) *) diff --git a/compiler/Values.ml b/compiler/Values.ml index c1ff9804..60cbcc8b 100644 --- a/compiler/Values.ml +++ b/compiler/Values.ml @@ -42,6 +42,7 @@ type sv_kind = | SynthInputGivenBack (** The value was given back upon ending one of the input abstractions *) | Global (** The value is a global *) + | KindConstGeneric (** The value is a const generic *) | LoopOutput (** The output of a loop (seen as a forward computation) *) | LoopGivenBack (** A value given back by a loop (when ending abstractions while going backwards) *) |