diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 12 | ||||
| -rw-r--r-- | compiler/FunsAnalysis.ml | 6 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 29 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsCore.ml | 7 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsJoinCtxs.ml | 10 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 41 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 32 | ||||
| -rw-r--r-- | compiler/PrePasses.ml | 2 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 1 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 221 | ||||
| -rw-r--r-- | compiler/Translate.ml | 1 |
13 files changed, 172 insertions, 194 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index d6a5f0fc..1f9c9117 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -509,8 +509,6 @@ and extract_function_call (meta : Meta.meta) (ctx : extraction_ctx) | Error (types, err) -> extract_generic_args meta ctx fmt TypeDeclId.Set.empty { generics with types }; - (* if !Config.fail_hard then craise __FILE__ __LINE__ meta err - else *) save_error __FILE__ __LINE__ (Some meta) err; F.pp_print_string fmt "(\"ERROR: ill-formed builtin: invalid number of filtering \ @@ -1876,8 +1874,8 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (global : global_decl) (body : fun_decl) (interface : bool) : unit = let meta = body.meta in - sanity_check __FILE__ __LINE__ body.is_global_decl_body body.meta; - sanity_check __FILE__ __LINE__ (body.signature.inputs = []) body.meta; + sanity_check __FILE__ __LINE__ body.is_global_decl_body meta; + sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta; (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; @@ -2232,7 +2230,8 @@ let extract_trait_impl_register_names (ctx : extraction_ctx) cassert __FILE__ __LINE__ (trait_impl.provided_methods = []) trait_impl.meta - ("Overriding provided methods is not supported yet (overriden methods: " + ("Overriding trait provided methods in trait implementations is not \ + supported yet (overriden methods: " ^ String.concat ", " (List.map fst trait_impl.provided_methods) ^ ")"); (* Everything is taken care of by {!extract_trait_decl_register_names} *but* @@ -2622,8 +2621,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) in extract_trait_impl_item ctx fmt fun_name ty -(** Extract a trait implementation -*) +(** Extract a trait implementation *) let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (impl : trait_impl) : unit = log#ldebug (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.llbc_name)); diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index cad469f9..f194d4e5 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -119,7 +119,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) method! visit_Call env call = (match call.func with | FnOpMove _ -> - (* Ignoring this: we lookup t he called function upon creating + (* Ignoring this: we lookup the called function upon creating the closure *) () | FnOpRegular func -> ( @@ -145,9 +145,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) end in (* Sanity check: global bodies don't contain stateful calls *) - sanity_check __FILE__ __LINE__ + cassert __FILE__ __LINE__ ((not f.is_global_decl_body) || not !stateful) - f.meta; + f.meta "Global definition containing a stateful call in its body"; let builtin_info = get_builtin_info f in let has_builtin_info = builtin_info <> None in group_has_builtin_info := !group_has_builtin_info || has_builtin_info; diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index b32261e6..e593ae75 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -443,8 +443,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - cassert __FILE__ __LINE__ !replaced meta - "Only one loan should have been given back"; + cassert __FILE__ __LINE__ !replaced meta "No loan updated"; (* Apply the reborrows *) apply_registered_reborrows ctx @@ -503,7 +502,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) let replaced : bool ref = ref false in let set_replaced () = cassert __FILE__ __LINE__ (not !replaced) meta - "Only one loan should have been updated"; + "Exacly one loan should be updated"; replaced := true in let obj = @@ -589,7 +588,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - cassert __FILE__ __LINE__ !replaced meta "Only one loan should be given back"; + cassert __FILE__ __LINE__ !replaced meta "No loan updated"; (* Return *) ctx @@ -608,7 +607,7 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id) let replaced : bool ref = ref false in let set_replaced () = cassert __FILE__ __LINE__ (not !replaced) meta - "Only one loan should be updated"; + "Exactly one loan should be updated"; replaced := true in let obj = @@ -673,8 +672,7 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id) (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - cassert __FILE__ __LINE__ !replaced meta - "Exactly one loan should be given back"; + cassert __FILE__ __LINE__ !replaced meta "No loan updated"; (* Return *) ctx @@ -1553,8 +1551,8 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) (* I don't think it is possible to have two-phase borrows involving borrows * returned by abstractions. I'm not sure how we could handle that anyway. *) craise __FILE__ __LINE__ meta - "Can't promote a shared loan to a mutable loan if the loan is inside \ - an abstraction" + "Can't promote a shared loan to a mutable loan if the loan is inside a \ + region abstraction" (** Helper function: see {!activate_reserved_mut_borrow}. @@ -1581,7 +1579,7 @@ let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id) (* This can't happen for sure *) craise __FILE__ __LINE__ meta "Can't promote a shared borrow to a mutable borrow if the borrow is \ - inside an abstraction" + inside a region abstraction" in (* Continue *) cf ctx @@ -1647,7 +1645,7 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) * returned by abstractions. I'm not sure how we could handle that anyway. *) craise __FILE__ __LINE__ meta "Can't activate a reserved mutable borrow referencing a loan inside\n\ - \ an abstraction" + \ a region abstraction" let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) (destructure_shared_values : bool) (ctx : eval_ctx) (abs0 : abs) : abs = @@ -2272,12 +2270,11 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (* Sanity check: there is no loan/borrows which appears in both abstractions, unless we allow to merge duplicates *) - if merge_funs = None then - (sanity_check __FILE__ __LINE__ - (BorrowId.Set.disjoint borrows0 borrows1) - meta; - sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1)) + if merge_funs = None then ( + sanity_check __FILE__ __LINE__ + (BorrowId.Set.disjoint borrows0 borrows1) meta; + sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1) meta); (* Merge. There are several cases: diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 92d8670a..6e65b11d 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -864,7 +864,7 @@ let update_intersecting_aproj_borrows (meta : Meta.meta) let ctx = obj#visit_eval_ctx None ctx in (* Check that we updated the context at least once *) cassert __FILE__ __LINE__ (Option.is_some !shared) meta - "Context was not updated at least once"; + "Context was not updated"; (* Return *) ctx diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index 2283e842..a5b3a021 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -256,12 +256,12 @@ module type PrimMatcher = sig end module type Matcher = sig + val meta : Meta.meta + (** Match two values. Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}. *) - val meta : Meta.meta - val match_typed_values : eval_ctx -> eval_ctx -> typed_value -> typed_value -> typed_value @@ -279,6 +279,8 @@ end Very annoying: functors only take modules as inputs... *) module type MatchCheckEquivState = sig + val meta : Meta.meta + (** [true] if we check equivalence between contexts, [false] if we match a source context with a target context. *) val check_equiv : bool @@ -299,7 +301,6 @@ module type MatchCheckEquivState = sig val aid_map : AbstractionId.InjSubst.t ref val lookup_shared_value_in_ctx0 : BorrowId.id -> typed_value val lookup_shared_value_in_ctx1 : BorrowId.id -> typed_value - val meta : Meta.meta end module type CheckEquivMatcher = sig diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index d97b05d0..de00cb93 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -491,8 +491,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) are not in the prefix anymore *) if DummyVarId.Set.mem b0 fixed_ids.dids then ( (* Still in the prefix: match the values *) - cassert __FILE__ __LINE__ (b0 = b1) meta - "Bindings are not the same. We are not in the prefix anymore"; + sanity_check __FILE__ __LINE__ (b0 = b1) meta; let b = b0 in let v = M.match_typed_values ctx0 ctx1 v0 v1 in let var = EBinding (BDummy b, v) in @@ -514,9 +513,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (* Variable bindings *must* be in the prefix and consequently their ids must be the same *) - cassert __FILE__ __LINE__ (b0 = b1) meta - "Variable bindings *must* be in the prefix and consequently their\n\ - \ ids must be the same"; + sanity_check __FILE__ __LINE__ (b0 = b1) meta; (* Match the values *) let b = b0 in let v = M.match_typed_values ctx0 ctx1 v0 v1 in @@ -537,8 +534,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (* Same as for the dummy values: there are two cases *) if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then ( (* Still in the prefix: the abstractions must be the same *) - cassert __FILE__ __LINE__ (abs0 = abs1) meta - "The abstractions are not the same"; + sanity_check __FILE__ __LINE__ (abs0 = abs1) meta; (* Continue *) abs :: join_prefixes env0' env1') else (* Not in the prefix anymore *) diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index bd271ff4..e710ed2b 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -827,13 +827,13 @@ end (* Very annoying: functors only take modules as inputs... *) module type MatchMoveState = sig + val meta : Meta.meta + (** The current loop *) val loop_id : LoopId.id (** The moved values *) val nvalues : typed_value list ref - - val meta : Meta.meta end (* We use this matcher to move values in environment. @@ -853,9 +853,9 @@ end indeed matches the resulting target environment: it will be re-checked later. *) module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct - (** Small utility *) let meta = S.meta + (** Small utility *) let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues let match_etys _ _ ty0 ty1 = @@ -959,6 +959,8 @@ end module MakeCheckEquivMatcher (S : MatchCheckEquivState) : CheckEquivMatcher = struct + let meta = S.meta + module MkGetSetM (Id : Identifiers.Id) = struct module Inj = Id.InjSubst @@ -1001,8 +1003,6 @@ struct (match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1)) end - let meta = S.meta - module GetSetRid = MkGetSetM (RegionId) let match_rid = GetSetRid.match_e "match_rid: " S.rid_map @@ -1383,15 +1383,15 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) | EBinding (BDummy b0, v0) :: env0', EBinding (BDummy b1, v1) :: env1' -> (* Sanity check: if the dummy value is an old value, the bindings must be the same and their values equal (and the borrows/loans/symbolic *) - if DummyVarId.Set.mem b0 fixed_ids.dids then - ((* Fixed values: the values must be equal *) - sanity_check __FILE__ __LINE__ (b0 = b1) meta; - sanity_check __FILE__ __LINE__ (v0 = v1) meta; - (* The ids present in the left value must be fixed *) - let ids, _ = compute_typed_value_ids v0 in - sanity_check __FILE__ __LINE__ - ((not S.check_equiv) || ids_are_fixed ids)) - meta; + if DummyVarId.Set.mem b0 fixed_ids.dids then ( + (* Fixed values: the values must be equal *) + sanity_check __FILE__ __LINE__ (b0 = b1) meta; + sanity_check __FILE__ __LINE__ (v0 = v1) meta; + (* The ids present in the left value must be fixed *) + let ids, _ = compute_typed_value_ids v0 in + sanity_check __FILE__ __LINE__ + ((not S.check_equiv) || ids_are_fixed ids) + meta); (* We still match the values - allows to compute mappings (which are the identity actually) *) let _ = M.match_typed_values ctx0 ctx1 v0 v1 in @@ -1457,9 +1457,16 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) } in Some maps - with Distinct msg -> - log#ldebug (lazy ("match_ctxs: distinct: " ^ msg)); - None + with + | Distinct msg -> + log#ldebug (lazy ("match_ctxs: distinct: " ^ msg ^ "\n")); + None + | ValueMatchFailure k -> + log#ldebug + (lazy + ("match_ctxs: distinct: ValueMatchFailure" ^ show_updt_env_kind k + ^ "\n")); + None let ctxs_are_equivalent (meta : Meta.meta) (fixed_ids : ids_sets) (ctx0 : eval_ctx) (ctx1 : eval_ctx) : bool = diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 93e56106..f2c0bcb1 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -483,7 +483,7 @@ let rec update_ctx_along_read_place (config : config) (meta : Meta.meta) (Some (Synth.mk_mplace meta prefix ctx)) | FailBottom (_, _, _) -> (* We can't expand {!Bottom} values while reading them *) - craise __FILE__ __LINE__ meta "Found [Bottom] while reading a place" + craise __FILE__ __LINE__ meta "Found bottom while reading a place" | FailBorrow _ -> craise __FILE__ __LINE__ meta "Could not read a borrow" in diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 8b6eeb6c..6e86e6a4 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -199,22 +199,22 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) | VSymbolic s, _ -> (* Check that the projection doesn't contain already ended regions, * if necessary *) - if check_symbolic_no_ended then - (let ty1 = s.sv_ty in - let rset1 = ctx.ended_regions in - let ty2 = ty in - let rset2 = regions in - log#ldebug - (lazy - ("projections_intersect:" ^ "\n- ty1: " ^ ty_to_string ctx ty1 - ^ "\n- rset1: " - ^ RegionId.Set.to_string None rset1 - ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: " - ^ RegionId.Set.to_string None rset2 - ^ "\n")); - sanity_check __FILE__ __LINE__ - (not (projections_intersect meta ty1 rset1 ty2 rset2))) - meta; + if check_symbolic_no_ended then ( + let ty1 = s.sv_ty in + let rset1 = ctx.ended_regions in + let ty2 = ty in + let rset2 = regions in + log#ldebug + (lazy + ("projections_intersect:" ^ "\n- ty1: " ^ ty_to_string ctx ty1 + ^ "\n- rset1: " + ^ RegionId.Set.to_string None rset1 + ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: " + ^ RegionId.Set.to_string None rset2 + ^ "\n")); + sanity_check __FILE__ __LINE__ + (not (projections_intersect meta ty1 rset1 ty2 rset2)) + meta); ASymbolic (AProjBorrows (s, ty)) | _ -> log#lerror diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml index 11cd89fc..0b39f64a 100644 --- a/compiler/PrePasses.ml +++ b/compiler/PrePasses.ml @@ -402,8 +402,8 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl = let check_visitor = object inherit [_] iter_statement as super - (* Remember the span of the statement we enter *) + (* Remember the span of the statement we enter *) method! visit_statement _ st = super#visit_statement st.meta st method! visit_var_id meta id = diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 12b3387a..9fa07029 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1989,6 +1989,7 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) : (List.concat (List.map (fun { f; loops } -> [ f :: loops ]) transl)) in let subgroups = ReorderDecls.group_reorder_fun_decls all_decls in + log#ldebug (lazy ("filter_loop_inputs: all_decls:\n\n" diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 4830f65a..0c30f44c 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -144,6 +144,7 @@ type loop_info = { (** 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; @@ -325,7 +326,7 @@ let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string = 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.fun_decl.meta) env v + 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 @@ -349,8 +350,7 @@ let pure_type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string = 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.fun_decl.meta) env false - "" " " e + 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 @@ -364,10 +364,9 @@ 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 ?(meta : Meta.meta option = None) (ctx : bs_ctx) - (p : Pure.typed_pattern) : string = +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 env p + 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 = @@ -386,7 +385,7 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string = let verbose = false in let indent = "" in let indent_incr = " " in - Print.Values.abs_to_string ~meta:(Some ctx.fun_decl.meta) env verbose indent + 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) : @@ -676,13 +675,13 @@ and translate_fwd_trait_instance_id (meta : Meta.meta) (type_infos : type_infos) (** 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.fun_decl.meta type_infos ty + 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.fun_decl.meta type_infos generics + translate_fwd_generic_args ctx.meta type_infos generics (** Translate a type, when some regions may have ended. @@ -775,7 +774,7 @@ let rec translate_back_ty (meta : Meta.meta) (type_infos : type_infos) 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.fun_decl.meta type_infos keep_region inside_mut ty + 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 = @@ -794,14 +793,14 @@ let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx = } let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit = - let meta = ctx.fun_decl.meta in + 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.fun_decl.meta in + let meta = ctx.meta in let ctx = mk_type_check_ctx ctx in PureTypeCheck.check_texpression meta ctx e @@ -811,9 +810,7 @@ let translate_fun_id_or_trait_method_ref (ctx : bs_ctx) | 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.fun_decl.meta type_infos trait_ref - 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) @@ -823,7 +820,7 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call) let calls = ctx.calls in sanity_check __FILE__ __LINE__ (not (V.FunCallId.Map.mem call_id calls)) - ctx.fun_decl.meta; + 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 } @@ -847,7 +844,7 @@ let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id) let abstractions = ctx.abstractions in sanity_check __FILE__ __LINE__ (not (V.AbstractionId.Map.mem abs.abs_id abstractions)) - ctx.fun_decl.meta; + ctx.meta; let abstractions = V.AbstractionId.Map.add abs.abs_id (abs, back_args) abstractions in @@ -953,22 +950,20 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref) in { info with is_rec = info.is_rec || Option.is_some lid } | FunId (FAssumed _) -> - compute_raw_fun_effect_info ctx.fun_decl.meta ctx.fun_ctx.fun_infos - fun_id lid gid) + 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.fun_decl.meta; + 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.fun_decl.meta "Unreachable") + | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable") (** Translate a function signature to a decomposed function signature. @@ -1514,7 +1509,7 @@ 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.fun_decl.meta + craise __FILE__ __LINE__ ctx.meta ("Could not find var for symbolic value: " ^ V.SymbolicValueId.to_string sv.sv_id) @@ -1564,7 +1559,7 @@ let symbolic_value_to_texpression (ctx : bs_ctx) (sv : V.symbolic_value) : 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.fun_decl.meta v in + 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 @@ -1578,12 +1573,12 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) (* 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.fun_decl.meta; - mk_simpl_tuple_texpression ctx.fun_decl.meta field_values + 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.fun_decl.meta ty in + 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 @@ -1594,20 +1589,18 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) let cons_ty = mk_arrows field_tys ty in let cons = { e = cons_e; ty = cons_ty } in (* Apply the constructor *) - mk_apps ctx.fun_decl.meta cons field_values) - | VBottom -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable" + 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.fun_decl.meta "Unreachable" - ) + | 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.fun_decl.meta ectx - bid + InterpreterBorrowsCore.lookup_shared_value ctx.meta ectx bid in translate sv | VReservedMutBorrow bid -> @@ -1615,8 +1608,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) * 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.fun_decl.meta ectx - bid + InterpreterBorrowsCore.lookup_shared_value ctx.meta ectx bid in translate sv | VMutBorrow (_, v) -> @@ -1663,7 +1655,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) 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.fun_decl.meta + cassert __FILE__ __LINE__ (field_values = []) ctx.meta "ADTs containing borrows are not supported yet"; None | TTuple -> @@ -1672,11 +1664,9 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) else (* Note that if there is exactly one field value, * [mk_simpl_tuple_rvalue] is the identity *) - let rv = - mk_simpl_tuple_texpression ctx.fun_decl.meta field_values - in + let rv = mk_simpl_tuple_texpression ctx.meta field_values in Some rv) - | ABottom -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable" + | 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 @@ -1694,7 +1684,7 @@ 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.fun_decl.meta "Unreachable" + 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) @@ -1706,7 +1696,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) None | AIgnoredMutLoan (_, _) -> (* There can be *inner* not ended mutable loans, but not outer ones *) - craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable" + craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedIgnoredMutLoan _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented @@ -1718,7 +1708,7 @@ 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.fun_decl.meta "Unreachable" + craise __FILE__ __LINE__ _ctx.meta "Unreachable" | AEndedMutBorrow (_, _) -> (* We collect consumed values: ignore *) None @@ -1737,7 +1727,7 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option = | V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) -> sanity_check __FILE__ __LINE__ (child_aproj = AIgnoredProjBorrows) - ctx.fun_decl.meta; + ctx.meta; (* The symbolic value was updated *) Some (symbolic_value_to_texpression ctx mnv) | V.AEndedProjLoans (_, _) -> @@ -1746,7 +1736,7 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option = raise Unimplemented | AEndedProjBorrows _ -> (* We consider consumed values *) None | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> - craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable" + craise __FILE__ __LINE__ ctx.meta "Unreachable" (** Convert the abstraction values in an abstraction to consumed values. @@ -1812,20 +1802,20 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) 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.fun_decl.meta + 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.fun_decl.meta; + 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.fun_decl.meta "Unreachable" + | 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 @@ -1841,14 +1831,14 @@ 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.fun_decl.meta "Unreachable" + 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.fun_decl.meta "Unreachable" + craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedIgnoredMutLoan _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented @@ -1860,7 +1850,7 @@ 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.fun_decl.meta "Unreachable" + craise __FILE__ __LINE__ ctx.meta "Unreachable" | AEndedMutBorrow (msv, _) -> (* Return the meta-symbolic-value *) let ctx, var = fresh_var_for_symbolic_value msv ctx in @@ -1882,14 +1872,14 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : (List.for_all (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows) child_projs) - ctx.fun_decl.meta "Nested borrows are not supported yet"; + 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.fun_decl.meta "Unreachable" + craise __FILE__ __LINE__ ctx.meta "Unreachable" (** Convert the abstraction values in an abstraction to given back values. @@ -2004,7 +1994,7 @@ 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 modune partie nad, we need to add a lambda for the state variable *) + (* 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 *) @@ -2013,13 +2003,13 @@ and translate_panic (ctx : bs_ctx) : texpression = (* 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.fun_decl.meta - error_failure_id ret_ty + 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.fun_decl.meta - error_failure_id output_ty + 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 *) @@ -2075,12 +2065,12 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option) | Some _ -> (* Backward function *) (* Sanity check *) - sanity_check __FILE__ __LINE__ (opt_v = None) ctx.fun_decl.meta; + 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.fun_decl.meta field_values + mk_simpl_tuple_texpression ctx.meta field_values in (* We may need to return a state * - error-monad: Return x @@ -2090,21 +2080,17 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option) let output = if effect_info.stateful then let state_rvalue = mk_state_texpression ctx.state_var in - mk_simpl_tuple_texpression ctx.fun_decl.meta [ state_rvalue; output ] + 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.fun_decl.meta output + 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.fun_decl.meta; + 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.fun_decl.meta; + 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 @@ -2128,7 +2114,7 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) 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.fun_decl.meta field_values + mk_simpl_tuple_texpression ctx.meta field_values in (* We may need to return a state @@ -2142,12 +2128,12 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) let output = if effect_info.stateful then let state_rvalue = mk_state_texpression ctx.state_var in - mk_simpl_tuple_texpression ctx.fun_decl.meta [ state_rvalue; output ] + 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.fun_decl.meta output) + (mk_result_return_texpression ctx.meta output) and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : texpression = @@ -2198,8 +2184,8 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : 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.fun_decl.meta decls_ctx fid call.regions_hierarchy sg + 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 @@ -2212,7 +2198,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : ctx_translate_fwd_generic_args ctx all_generics in let tr_self = - translate_fwd_trait_instance_id ctx.fun_decl.meta + translate_fwd_trait_instance_id ctx.meta ctx.type_ctx.type_infos tr_self in (tr_self, all_generics) @@ -2333,7 +2319,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : | S.Unop E.Neg -> ( match args with | [ arg ] -> - let int_ty = ty_as_integer ctx.fun_decl.meta arg.ty in + 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 = @@ -2348,7 +2334,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : 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.fun_decl.meta "Unreachable") + | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable") | S.Unop (E.Cast cast_kind) -> ( match cast_kind with | CastScalar (src_ty, tgt_ty) -> @@ -2366,18 +2352,16 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : 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.fun_decl.meta "TODO: function casts") + craise __FILE__ __LINE__ ctx.meta "TODO: function casts") | S.Binop binop -> ( match args with | [ arg0; arg1 ] -> - let int_ty0 = ty_as_integer ctx.fun_decl.meta arg0.ty in - let int_ty1 = ty_as_integer ctx.fun_decl.meta arg1.ty in + 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.fun_decl.meta); + | _ -> sanity_check __FILE__ __LINE__ (int_ty0 = int_ty1) ctx.meta); let effect_info = { can_fail = ExpressionsUtils.binop_can_fail binop; @@ -2390,7 +2374,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : 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.fun_decl.meta "Unreachable") + | _ -> 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 @@ -2399,7 +2383,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : 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.fun_decl.meta func args in + let call = mk_apps ctx.meta func args in (* Translate the next expression *) let next_e = translate_expression e ctx in (* Put together *) @@ -2433,7 +2417,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) ^ "\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.fun_decl.meta) ectx + ^ 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 @@ -2447,7 +2431,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) for a parent backward function. *) let bid = Option.get ctx.bid in - sanity_check __FILE__ __LINE__ (rg_id = bid) ctx.fun_decl.meta; + sanity_check __FILE__ __LINE__ (rg_id = bid) ctx.meta; (* First, introduce the given back variables. @@ -2497,7 +2481,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) (fun (var, v) -> sanity_check __FILE__ __LINE__ ((var : var).ty = (v : texpression).ty) - ctx.fun_decl.meta) + ctx.meta) variables_values; (* Translate the next expression *) let next_e = translate_expression e ctx in @@ -2518,7 +2502,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) | S.Fun (fun_id, _) -> fun_id | Unop _ | Binop _ -> (* Those don't have backward functions *) - craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable" + 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 @@ -2580,7 +2564,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) ^ "\nfunc type: " ^ pure_ty_to_string ctx func.ty ^ "\n\nargs:\n" ^ String.concat "\n" args)); - let call = mk_apps ctx.fun_decl.meta func args in + 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) @@ -2591,8 +2575,8 @@ and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs) (* 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.fun_decl.meta; - sanity_check __FILE__ __LINE__ (outputs = []) ctx.fun_decl.meta; + sanity_check __FILE__ __LINE__ (inputs = []) ctx.meta; + sanity_check __FILE__ __LINE__ (outputs = []) ctx.meta; (* Translate the next expression *) translate_expression e ctx @@ -2634,7 +2618,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) (* 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.fun_decl.meta + 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 @@ -2653,8 +2637,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) ^ 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.fun_decl.meta) + 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 @@ -2671,9 +2654,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) 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.fun_decl.meta; + 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) *) @@ -2743,7 +2724,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) match func with | None -> next_e | Some func -> - let call = mk_apps ctx.fun_decl.meta func args in + 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 @@ -2800,7 +2781,7 @@ and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value) 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.fun_decl.meta func args 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) @@ -2815,7 +2796,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) | V.SeLiteral _ -> (* We do not *register* symbolic expansions to literal values in the symbolic ADT *) - craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable" + 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 *) @@ -2828,11 +2809,11 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) next_e | SeAdt _ -> (* Should be in the [ExpandAdt] case *) - craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable") + 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.fun_decl.meta "Unreachable" + | [] -> craise __FILE__ __LINE__ ctx.meta "Unreachable" | [ (variant_id, svl, branch) ] when not (TypesUtils.ty_is_custom_adt sv.V.sv_ty @@ -2873,7 +2854,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) (* Sanity check *) sanity_check __FILE__ __LINE__ (List.for_all (fun br -> br.branch.ty = ty) branches) - ctx.fun_decl.meta; + ctx.meta; (* Return *) { e; ty }) | ExpandBool (true_e, false_e) -> @@ -2893,7 +2874,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) ^ 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.fun_decl.meta; + 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) : @@ -2920,7 +2901,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) let ty = otherwise.branch.ty in sanity_check __FILE__ __LINE__ (List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches) - ctx.fun_decl.meta; + ctx.meta; { e; ty } (* Translate and [ExpandAdt] when there is no branching (i.e., one branch). @@ -2995,14 +2976,14 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) * 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.fun_decl.meta scrutinee.ty in + 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.fun_decl.meta proj scrutinee + mk_app ctx.meta proj scrutinee in let id_var_pairs = FieldId.mapi (fun fid v -> (fid, v)) vars in let monadic = false in @@ -3023,7 +3004,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) let var = match vars with | [ v ] -> v - | _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable" + | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable" in (* We simply introduce an assignment - the box type is the * identity when extracted ([box a = a]) *) @@ -3037,7 +3018,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) * 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.fun_decl.meta + craise __FILE__ __LINE__ ctx.meta "Attempt to expand a non-expandable value" and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) @@ -3075,9 +3056,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) | 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.fun_decl.meta type_infos trait_ref - 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 } @@ -3218,7 +3197,7 @@ and translate_forward_end (ectx : C.eval_ctx) else pure_fwd_var :: back_vars in let vars = List.map mk_texpression_from_var vars in - let ret = mk_simpl_tuple_texpression ctx.fun_decl.meta 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 = @@ -3229,10 +3208,8 @@ and translate_forward_end (ectx : C.eval_ctx) in let state_var = List.map mk_texpression_from_var state_var in - let ret = - mk_simpl_tuple_texpression ctx.fun_decl.meta (state_var @ [ ret ]) - in - let ret = mk_result_return_texpression ctx.fun_decl.meta ret 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 *) @@ -3405,7 +3382,7 @@ and translate_forward_end (ectx : C.eval_ctx) 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.fun_decl.meta func args in + let call = mk_apps ctx.meta func args in call in @@ -3464,7 +3441,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = (fun (sv : V.symbolic_value) -> V.SymbolicValueId.Map.mem sv.sv_id ctx.sv_to_var) loop.input_svalues) - ctx.fun_decl.meta; + ctx.meta; (* Translate the loop inputs *) let inputs = @@ -3486,7 +3463,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = (fun ty -> cassert __FILE__ __LINE__ (not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty)) - !ctx.fun_decl.meta "The types shouldn't contain borrows"; + !ctx.meta "The types shouldn't contain borrows"; ctx_translate_fwd_ty !ctx ty) tys) loop.rg_to_given_back_tys @@ -3567,7 +3544,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = let ctx = sanity_check __FILE__ __LINE__ (not (LoopId.Map.mem loop_id ctx.loops)) - ctx.fun_decl.meta; + 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 diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 4c0f2e0d..348183c5 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -127,6 +127,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) let ctx = { + meta = fdef.meta; decls_ctx = trans_ctx; SymbolicToPure.bid = None; sg; |